The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^2).

(0) Obligation:

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^2).


The TRS R consists of the following rules:

min(x, 0) → 0
min(0, y) → 0
min(s(x), s(y)) → s(min(x, y))
max(x, 0) → x
max(0, y) → y
max(s(x), s(y)) → s(max(x, y))
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
gcd(s(x), 0) → s(x)
gcd(0, s(x)) → s(x)
gcd(s(x), s(y)) → gcd(-(max(x, y), min(x, y)), s(min(x, y)))

Rewrite Strategy: INNERMOST

(1) TrsToWeightedTrsProof (BOTH BOUNDS(ID, ID) transformation)

Transformed TRS to weighted TRS

(2) Obligation:

The Runtime Complexity (innermost) of the given CpxWeightedTrs could be proven to be BOUNDS(1, n^2).


The TRS R consists of the following rules:

min(x, 0) → 0 [1]
min(0, y) → 0 [1]
min(s(x), s(y)) → s(min(x, y)) [1]
max(x, 0) → x [1]
max(0, y) → y [1]
max(s(x), s(y)) → s(max(x, y)) [1]
-(x, 0) → x [1]
-(s(x), s(y)) → -(x, y) [1]
gcd(s(x), 0) → s(x) [1]
gcd(0, s(x)) → s(x) [1]
gcd(s(x), s(y)) → gcd(-(max(x, y), min(x, y)), s(min(x, y))) [1]

Rewrite Strategy: INNERMOST

(3) CpxWeightedTrsRenamingProof (BOTH BOUNDS(ID, ID) transformation)

Renamed defined symbols to avoid conflicts with arithmetic symbols:

- => minus

(4) Obligation:

The Runtime Complexity (innermost) of the given CpxWeightedTrs could be proven to be BOUNDS(1, n^2).


The TRS R consists of the following rules:

min(x, 0) → 0 [1]
min(0, y) → 0 [1]
min(s(x), s(y)) → s(min(x, y)) [1]
max(x, 0) → x [1]
max(0, y) → y [1]
max(s(x), s(y)) → s(max(x, y)) [1]
minus(x, 0) → x [1]
minus(s(x), s(y)) → minus(x, y) [1]
gcd(s(x), 0) → s(x) [1]
gcd(0, s(x)) → s(x) [1]
gcd(s(x), s(y)) → gcd(minus(max(x, y), min(x, y)), s(min(x, y))) [1]

Rewrite Strategy: INNERMOST

(5) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(6) Obligation:

Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

min(x, 0) → 0 [1]
min(0, y) → 0 [1]
min(s(x), s(y)) → s(min(x, y)) [1]
max(x, 0) → x [1]
max(0, y) → y [1]
max(s(x), s(y)) → s(max(x, y)) [1]
minus(x, 0) → x [1]
minus(s(x), s(y)) → minus(x, y) [1]
gcd(s(x), 0) → s(x) [1]
gcd(0, s(x)) → s(x) [1]
gcd(s(x), s(y)) → gcd(minus(max(x, y), min(x, y)), s(min(x, y))) [1]

The TRS has the following type information:

min :: 0:s → 0:s → 0:s 0 :: 0:s s :: 0:s → 0:s max :: 0:s → 0:s → 0:s minus :: 0:s → 0:s → 0:s gcd :: 0:s → 0:s → 0:s

Rewrite Strategy: INNERMOST

(7) CompletionProof (UPPER BOUND(ID) transformation)

The TRS is a completely defined constructor system, as every type has a constant constructor and the following rules were added:

minus(v0, v1) → null_minus [0]
gcd(v0, v1) → null_gcd [0]
min(v0, v1) → null_min [0]
max(v0, v1) → null_max [0]

And the following fresh constants:

null_minus, null_gcd, null_min, null_max

(8) Obligation:

Runtime Complexity Weighted TRS where all functions are completely defined. The underlying TRS is:

Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: min(x, 0) → 0 [1] min(0, y) → 0 [1] min(s(x), s(y)) → s(min(x, y)) [1] max(x, 0) → x [1] max(0, y) → y [1] max(s(x), s(y)) → s(max(x, y)) [1] minus(x, 0) → x [1] minus(s(x), s(y)) → minus(x, y) [1] gcd(s(x), 0) → s(x) [1] gcd(0, s(x)) → s(x) [1] gcd(s(x), s(y)) → gcd(minus(max(x, y), min(x, y)), s(min(x, y))) [1] minus(v0, v1) → null_minus [0] gcd(v0, v1) → null_gcd [0] min(v0, v1) → null_min [0] max(v0, v1) → null_max [0] The TRS has the following type information: min :: 0:s:null_minus:null_gcd:null_min:null_max → 0:s:null_minus:null_gcd:null_min:null_max → 0:s:null_minus:null_gcd:null_min:null_max 0 :: 0:s:null_minus:null_gcd:null_min:null_max s :: 0:s:null_minus:null_gcd:null_min:null_max → 0:s:null_minus:null_gcd:null_min:null_max max :: 0:s:null_minus:null_gcd:null_min:null_max → 0:s:null_minus:null_gcd:null_min:null_max → 0:s:null_minus:null_gcd:null_min:null_max minus :: 0:s:null_minus:null_gcd:null_min:null_max → 0:s:null_minus:null_gcd:null_min:null_max → 0:s:null_minus:null_gcd:null_min:null_max gcd :: 0:s:null_minus:null_gcd:null_min:null_max → 0:s:null_minus:null_gcd:null_min:null_max → 0:s:null_minus:null_gcd:null_min:null_max null_minus :: 0:s:null_minus:null_gcd:null_min:null_max null_gcd :: 0:s:null_minus:null_gcd:null_min:null_max null_min :: 0:s:null_minus:null_gcd:null_min:null_max null_max :: 0:s:null_minus:null_gcd:null_min:null_max Rewrite Strategy: INNERMOST

(9) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID) transformation)

Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction.
The constant constructors are abstracted as follows:

0 => 0
null_minus => 0
null_gcd => 0
null_min => 0
null_max => 0

(10) Obligation:

Complexity RNTS consisting of the following rules:

gcd(z, z') -{ 1 }→ gcd(minus(max(x, y), min(x, y)), 1 + min(x, y)) :|: z' = 1 + y, x >= 0, y >= 0, z = 1 + x
gcd(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
gcd(z, z') -{ 1 }→ 1 + x :|: x >= 0, z = 1 + x, z' = 0
gcd(z, z') -{ 1 }→ 1 + x :|: z' = 1 + x, x >= 0, z = 0
max(z, z') -{ 1 }→ x :|: x >= 0, z = x, z' = 0
max(z, z') -{ 1 }→ y :|: y >= 0, z = 0, z' = y
max(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
max(z, z') -{ 1 }→ 1 + max(x, y) :|: z' = 1 + y, x >= 0, y >= 0, z = 1 + x
min(z, z') -{ 1 }→ 0 :|: x >= 0, z = x, z' = 0
min(z, z') -{ 1 }→ 0 :|: y >= 0, z = 0, z' = y
min(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
min(z, z') -{ 1 }→ 1 + min(x, y) :|: z' = 1 + y, x >= 0, y >= 0, z = 1 + x
minus(z, z') -{ 1 }→ x :|: x >= 0, z = x, z' = 0
minus(z, z') -{ 1 }→ minus(x, y) :|: z' = 1 + y, x >= 0, y >= 0, z = 1 + x
minus(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1

Only complete derivations are relevant for the runtime complexity.

(11) CompleteCoflocoProof (EQUIVALENT transformation)

Transformed the RNTS (where only complete derivations are relevant) into cost relations for CoFloCo:

eq(start(V, V1),0,[min(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1),0,[max(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1),0,[minus(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1),0,[gcd(V, V1, Out)],[V >= 0,V1 >= 0]). eq(min(V, V1, Out),1,[],[Out = 0,V2 >= 0,V = V2,V1 = 0]). eq(min(V, V1, Out),1,[],[Out = 0,V3 >= 0,V = 0,V1 = V3]). eq(min(V, V1, Out),1,[min(V4, V5, Ret1)],[Out = 1 + Ret1,V1 = 1 + V5,V4 >= 0,V5 >= 0,V = 1 + V4]). eq(max(V, V1, Out),1,[],[Out = V6,V6 >= 0,V = V6,V1 = 0]). eq(max(V, V1, Out),1,[],[Out = V7,V7 >= 0,V = 0,V1 = V7]). eq(max(V, V1, Out),1,[max(V8, V9, Ret11)],[Out = 1 + Ret11,V1 = 1 + V9,V8 >= 0,V9 >= 0,V = 1 + V8]). eq(minus(V, V1, Out),1,[],[Out = V10,V10 >= 0,V = V10,V1 = 0]). eq(minus(V, V1, Out),1,[minus(V11, V12, Ret)],[Out = Ret,V1 = 1 + V12,V11 >= 0,V12 >= 0,V = 1 + V11]). eq(gcd(V, V1, Out),1,[],[Out = 1 + V13,V13 >= 0,V = 1 + V13,V1 = 0]). eq(gcd(V, V1, Out),1,[],[Out = 1 + V14,V1 = 1 + V14,V14 >= 0,V = 0]). eq(gcd(V, V1, Out),1,[max(V15, V16, Ret00),min(V15, V16, Ret01),minus(Ret00, Ret01, Ret0),min(V15, V16, Ret111),gcd(Ret0, 1 + Ret111, Ret2)],[Out = Ret2,V1 = 1 + V16,V15 >= 0,V16 >= 0,V = 1 + V15]). eq(minus(V, V1, Out),0,[],[Out = 0,V17 >= 0,V18 >= 0,V = V17,V1 = V18]). eq(gcd(V, V1, Out),0,[],[Out = 0,V19 >= 0,V20 >= 0,V = V19,V1 = V20]). eq(min(V, V1, Out),0,[],[Out = 0,V21 >= 0,V22 >= 0,V = V21,V1 = V22]). eq(max(V, V1, Out),0,[],[Out = 0,V23 >= 0,V24 >= 0,V = V23,V1 = V24]). input_output_vars(min(V,V1,Out),[V,V1],[Out]). input_output_vars(max(V,V1,Out),[V,V1],[Out]). input_output_vars(minus(V,V1,Out),[V,V1],[Out]). input_output_vars(gcd(V,V1,Out),[V,V1],[Out]).

CoFloCo proof output:
Preprocessing Cost Relations
=====================================

#### Computed strongly connected components
0. recursive : [max/3]
1. recursive : [min/3]
2. recursive : [minus/3]
3. recursive : [gcd/3]
4. non_recursive : [start/2]

#### Obtained direct recursion through partial evaluation
0. SCC is partially evaluated into max/3
1. SCC is partially evaluated into min/3
2. SCC is partially evaluated into minus/3
3. SCC is partially evaluated into gcd/3
4. SCC is partially evaluated into start/2

Control-Flow Refinement of Cost Relations
=====================================

### Specialization of cost equations max/3
* CE 13 is refined into CE [21]
* CE 10 is refined into CE [22]
* CE 11 is refined into CE [23]
* CE 12 is refined into CE [24]


### Cost equations --> "Loop" of max/3
* CEs [24] --> Loop 16
* CEs [21] --> Loop 17
* CEs [22] --> Loop 18
* CEs [23] --> Loop 19

### Ranking functions of CR max(V,V1,Out)
* RF of phase [16]: [V,V1]

#### Partial ranking functions of CR max(V,V1,Out)
* Partial RF of phase [16]:
- RF of loop [16:1]:
V
V1


### Specialization of cost equations min/3
* CE 6 is refined into CE [25]
* CE 7 is refined into CE [26]
* CE 9 is refined into CE [27]
* CE 8 is refined into CE [28]


### Cost equations --> "Loop" of min/3
* CEs [28] --> Loop 20
* CEs [25] --> Loop 21
* CEs [26,27] --> Loop 22

### Ranking functions of CR min(V,V1,Out)
* RF of phase [20]: [V,V1]

#### Partial ranking functions of CR min(V,V1,Out)
* Partial RF of phase [20]:
- RF of loop [20:1]:
V
V1


### Specialization of cost equations minus/3
* CE 16 is refined into CE [29]
* CE 14 is refined into CE [30]
* CE 15 is refined into CE [31]


### Cost equations --> "Loop" of minus/3
* CEs [31] --> Loop 23
* CEs [29] --> Loop 24
* CEs [30] --> Loop 25

### Ranking functions of CR minus(V,V1,Out)
* RF of phase [23]: [V,V1]

#### Partial ranking functions of CR minus(V,V1,Out)
* Partial RF of phase [23]:
- RF of loop [23:1]:
V
V1


### Specialization of cost equations gcd/3
* CE 20 is refined into CE [32]
* CE 17 is refined into CE [33]
* CE 18 is refined into CE [34]
* CE 19 is refined into CE [35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,65,66,67,68]


### Cost equations --> "Loop" of gcd/3
* CEs [52] --> Loop 26
* CEs [60] --> Loop 27
* CEs [62] --> Loop 28
* CEs [54] --> Loop 29
* CEs [46] --> Loop 30
* CEs [51] --> Loop 31
* CEs [59] --> Loop 32
* CEs [61] --> Loop 33
* CEs [67] --> Loop 34
* CEs [53] --> Loop 35
* CEs [45] --> Loop 36
* CEs [48,50] --> Loop 37
* CEs [40,42,44,56,58,64,66,68] --> Loop 38
* CEs [37] --> Loop 39
* CEs [38] --> Loop 40
* CEs [35] --> Loop 41
* CEs [36,39,41,43,47,49,55,57,63,65] --> Loop 42
* CEs [32] --> Loop 43
* CEs [33] --> Loop 44
* CEs [34] --> Loop 45

### Ranking functions of CR gcd(V,V1,Out)
* RF of phase [26,27,28,29,30,38]: [V+V1-3]
* RF of phase [39,41]: [V+V1-1]

#### Partial ranking functions of CR gcd(V,V1,Out)
* Partial RF of phase [26,27,28,29,30,38]:
- RF of loop [26:1,28:1,30:1,38:1]:
V-1 depends on loops [27:1,29:1]
- RF of loop [27:1,28:1,29:1,38:1]:
V+V1-3
* Partial RF of phase [39,41]:
- RF of loop [39:1]:
V depends on loops [41:1]
- RF of loop [41:1]:
V+V1-1


### Specialization of cost equations start/2
* CE 2 is refined into CE [69,70]
* CE 3 is refined into CE [71,72,73,74,75,76]
* CE 4 is refined into CE [77,78,79]
* CE 5 is refined into CE [80,81,82,83,84,85]


### Cost equations --> "Loop" of start/2
* CEs [84] --> Loop 46
* CEs [72,77,81] --> Loop 47
* CEs [69,70,71,73,74,75,76,78,79,80,82,83,85] --> Loop 48

### Ranking functions of CR start(V,V1)

#### Partial ranking functions of CR start(V,V1)


Computing Bounds
=====================================

#### Cost of chains of max(V,V1,Out):
* Chain [[16],19]: 1*it(16)+1
Such that:it(16) =< V

with precondition: [V1=Out,V>=1,V1>=V]

* Chain [[16],18]: 1*it(16)+1
Such that:it(16) =< V1

with precondition: [V=Out,V1>=1,V>=V1]

* Chain [[16],17]: 1*it(16)+0
Such that:it(16) =< Out

with precondition: [Out>=1,V>=Out,V1>=Out]

* Chain [19]: 1
with precondition: [V=0,V1=Out,V1>=0]

* Chain [18]: 1
with precondition: [V1=0,V=Out,V>=0]

* Chain [17]: 0
with precondition: [Out=0,V>=0,V1>=0]


#### Cost of chains of min(V,V1,Out):
* Chain [[20],22]: 1*it(20)+1
Such that:it(20) =< Out

with precondition: [Out>=1,V>=Out,V1>=Out]

* Chain [[20],21]: 1*it(20)+1
Such that:it(20) =< Out

with precondition: [V1=Out,V1>=1,V>=V1]

* Chain [22]: 1
with precondition: [Out=0,V>=0,V1>=0]

* Chain [21]: 1
with precondition: [V1=0,Out=0,V>=0]


#### Cost of chains of minus(V,V1,Out):
* Chain [[23],25]: 1*it(23)+1
Such that:it(23) =< V1

with precondition: [V=Out+V1,V1>=1,V>=V1]

* Chain [[23],24]: 1*it(23)+0
Such that:it(23) =< V1

with precondition: [Out=0,V>=1,V1>=1]

* Chain [25]: 1
with precondition: [V1=0,V=Out,V>=0]

* Chain [24]: 0
with precondition: [Out=0,V>=0,V1>=0]


#### Cost of chains of gcd(V,V1,Out):
* Chain [[39,41],45]: 5*it(39)+5*it(41)+1
Such that:aux(11) =< V
aux(12) =< V+V1
aux(13) =< V1
it(39) =< aux(12)
it(41) =< aux(12)
it(39) =< aux(13)+aux(11)

with precondition: [Out=1,V>=1,V1>=1]

* Chain [[39,41],43]: 5*it(39)+5*it(41)+0
Such that:aux(14) =< V
aux(15) =< V+V1
aux(16) =< V1
it(39) =< aux(15)
it(41) =< aux(15)
it(39) =< aux(16)+aux(14)

with precondition: [Out=0,V>=1,V1>=1]

* Chain [[39,41],42,45]: 5*it(39)+14*it(41)+9*s(7)+5
Such that:aux(22) =< 1
aux(23) =< V
aux(24) =< V+V1
aux(25) =< V1
it(41) =< aux(24)
s(7) =< aux(22)
it(39) =< aux(24)
it(39) =< aux(25)+aux(23)

with precondition: [Out=1,V>=1,V1>=1,V+V1>=3]

* Chain [[39,41],42,43]: 5*it(39)+14*it(41)+9*s(7)+4
Such that:aux(22) =< 1
aux(26) =< V
aux(27) =< V+V1
aux(28) =< V1
it(41) =< aux(27)
s(7) =< aux(22)
it(39) =< aux(27)
it(39) =< aux(28)+aux(26)

with precondition: [Out=0,V>=1,V1>=1,V+V1>=3]

* Chain [[39,41],40,45]: 5*it(39)+5*it(41)+5
Such that:aux(29) =< V
aux(30) =< V+V1
aux(31) =< V1
it(39) =< aux(30)
it(41) =< aux(30)
it(39) =< aux(31)+aux(29)

with precondition: [Out=1,V>=1,V1>=1,V+V1>=3]

* Chain [[39,41],40,43]: 5*it(39)+5*it(41)+4
Such that:aux(32) =< V
aux(33) =< V+V1
aux(34) =< V1
it(39) =< aux(33)
it(41) =< aux(33)
it(39) =< aux(34)+aux(32)

with precondition: [Out=0,V>=1,V1>=1,V+V1>=3]

* Chain [[26,27,28,29,30,38],[39,41],45]: 18*it(26)+18*it(27)+5*it(39)+2*s(112)+3*s(113)+8*s(114)+1*s(117)+4*s(119)+1*s(122)+28*s(123)+1*s(125)+3*s(134)+1
Such that:aux(90) =< V
aux(91) =< V+V1
aux(92) =< V1
it(39) =< aux(91)
it(27) =< aux(91)
it(39) =< aux(91)+aux(91)
it(26) =< aux(91)
aux(59) =< aux(91)
aux(56) =< aux(92)
aux(65) =< aux(91)-1
it(26) =< aux(92)+aux(92)+aux(90)
s(117) =< it(27)*aux(91)
s(116) =< aux(92)+aux(92)+aux(90)
s(135) =< aux(92)+aux(92)+aux(90)
s(120) =< it(27)*aux(59)
s(125) =< it(27)*aux(59)
s(124) =< it(26)*aux(59)
s(115) =< it(26)*aux(56)
s(135) =< it(26)*aux(59)
s(112) =< it(26)*aux(56)
s(122) =< it(26)*aux(65)
s(116) =< it(26)*aux(92)
s(123) =< s(124)
s(114) =< s(115)
s(134) =< s(135)
s(119) =< s(120)
s(113) =< s(116)

with precondition: [Out=1,V>=2,V1>=2]

* Chain [[26,27,28,29,30,38],[39,41],43]: 18*it(26)+18*it(27)+5*it(39)+2*s(112)+3*s(113)+8*s(114)+1*s(117)+4*s(119)+1*s(122)+28*s(123)+1*s(125)+3*s(134)+0
Such that:aux(93) =< V
aux(94) =< V+V1
aux(95) =< V1
it(39) =< aux(94)
it(27) =< aux(94)
it(39) =< aux(94)+aux(94)
it(26) =< aux(94)
aux(59) =< aux(94)
aux(56) =< aux(95)
aux(65) =< aux(94)-1
it(26) =< aux(95)+aux(95)+aux(93)
s(117) =< it(27)*aux(94)
s(116) =< aux(95)+aux(95)+aux(93)
s(135) =< aux(95)+aux(95)+aux(93)
s(120) =< it(27)*aux(59)
s(125) =< it(27)*aux(59)
s(124) =< it(26)*aux(59)
s(115) =< it(26)*aux(56)
s(135) =< it(26)*aux(59)
s(112) =< it(26)*aux(56)
s(122) =< it(26)*aux(65)
s(116) =< it(26)*aux(95)
s(123) =< s(124)
s(114) =< s(115)
s(134) =< s(135)
s(119) =< s(120)
s(113) =< s(116)

with precondition: [Out=0,V>=2,V1>=2]

* Chain [[26,27,28,29,30,38],[39,41],42,45]: 18*it(26)+27*it(27)+5*it(39)+9*s(7)+2*s(112)+3*s(113)+8*s(114)+1*s(117)+4*s(119)+1*s(122)+28*s(123)+1*s(125)+3*s(134)+5
Such that:aux(22) =< 1
aux(96) =< V
aux(97) =< V+V1
aux(98) =< V1
it(27) =< aux(97)
s(7) =< aux(22)
it(39) =< aux(97)
it(39) =< aux(97)+aux(97)
it(26) =< aux(97)
aux(59) =< aux(97)
aux(56) =< aux(98)
aux(65) =< aux(97)-1
it(26) =< aux(98)+aux(98)+aux(96)
s(117) =< it(27)*aux(97)
s(116) =< aux(98)+aux(98)+aux(96)
s(135) =< aux(98)+aux(98)+aux(96)
s(120) =< it(27)*aux(59)
s(125) =< it(27)*aux(59)
s(124) =< it(26)*aux(59)
s(115) =< it(26)*aux(56)
s(135) =< it(26)*aux(59)
s(112) =< it(26)*aux(56)
s(122) =< it(26)*aux(65)
s(116) =< it(26)*aux(98)
s(123) =< s(124)
s(114) =< s(115)
s(134) =< s(135)
s(119) =< s(120)
s(113) =< s(116)

with precondition: [Out=1,V>=2,V1>=2]

* Chain [[26,27,28,29,30,38],[39,41],42,43]: 18*it(26)+27*it(27)+5*it(39)+9*s(7)+2*s(112)+3*s(113)+8*s(114)+1*s(117)+4*s(119)+1*s(122)+28*s(123)+1*s(125)+3*s(134)+4
Such that:aux(22) =< 1
aux(99) =< V
aux(100) =< V+V1
aux(101) =< V1
it(27) =< aux(100)
s(7) =< aux(22)
it(39) =< aux(100)
it(39) =< aux(100)+aux(100)
it(26) =< aux(100)
aux(59) =< aux(100)
aux(56) =< aux(101)
aux(65) =< aux(100)-1
it(26) =< aux(101)+aux(101)+aux(99)
s(117) =< it(27)*aux(100)
s(116) =< aux(101)+aux(101)+aux(99)
s(135) =< aux(101)+aux(101)+aux(99)
s(120) =< it(27)*aux(59)
s(125) =< it(27)*aux(59)
s(124) =< it(26)*aux(59)
s(115) =< it(26)*aux(56)
s(135) =< it(26)*aux(59)
s(112) =< it(26)*aux(56)
s(122) =< it(26)*aux(65)
s(116) =< it(26)*aux(101)
s(123) =< s(124)
s(114) =< s(115)
s(134) =< s(135)
s(119) =< s(120)
s(113) =< s(116)

with precondition: [Out=0,V>=2,V1>=2]

* Chain [[26,27,28,29,30,38],[39,41],40,45]: 18*it(26)+18*it(27)+5*it(39)+2*s(112)+3*s(113)+8*s(114)+1*s(117)+4*s(119)+1*s(122)+28*s(123)+1*s(125)+3*s(134)+5
Such that:aux(102) =< V
aux(103) =< V+V1
aux(104) =< V1
it(39) =< aux(103)
it(27) =< aux(103)
it(39) =< aux(103)+aux(103)
it(26) =< aux(103)
aux(59) =< aux(103)
aux(56) =< aux(104)
aux(65) =< aux(103)-1
it(26) =< aux(104)+aux(104)+aux(102)
s(117) =< it(27)*aux(103)
s(116) =< aux(104)+aux(104)+aux(102)
s(135) =< aux(104)+aux(104)+aux(102)
s(120) =< it(27)*aux(59)
s(125) =< it(27)*aux(59)
s(124) =< it(26)*aux(59)
s(115) =< it(26)*aux(56)
s(135) =< it(26)*aux(59)
s(112) =< it(26)*aux(56)
s(122) =< it(26)*aux(65)
s(116) =< it(26)*aux(104)
s(123) =< s(124)
s(114) =< s(115)
s(134) =< s(135)
s(119) =< s(120)
s(113) =< s(116)

with precondition: [Out=1,V>=2,V1>=2]

* Chain [[26,27,28,29,30,38],[39,41],40,43]: 18*it(26)+18*it(27)+5*it(39)+2*s(112)+3*s(113)+8*s(114)+1*s(117)+4*s(119)+1*s(122)+28*s(123)+1*s(125)+3*s(134)+4
Such that:aux(105) =< V
aux(106) =< V+V1
aux(107) =< V1
it(39) =< aux(106)
it(27) =< aux(106)
it(39) =< aux(106)+aux(106)
it(26) =< aux(106)
aux(59) =< aux(106)
aux(56) =< aux(107)
aux(65) =< aux(106)-1
it(26) =< aux(107)+aux(107)+aux(105)
s(117) =< it(27)*aux(106)
s(116) =< aux(107)+aux(107)+aux(105)
s(135) =< aux(107)+aux(107)+aux(105)
s(120) =< it(27)*aux(59)
s(125) =< it(27)*aux(59)
s(124) =< it(26)*aux(59)
s(115) =< it(26)*aux(56)
s(135) =< it(26)*aux(59)
s(112) =< it(26)*aux(56)
s(122) =< it(26)*aux(65)
s(116) =< it(26)*aux(107)
s(123) =< s(124)
s(114) =< s(115)
s(134) =< s(135)
s(119) =< s(120)
s(113) =< s(116)

with precondition: [Out=0,V>=2,V1>=2]

* Chain [[26,27,28,29,30,38],45]: 18*it(26)+10*it(27)+2*s(112)+3*s(113)+8*s(114)+1*s(117)+3*s(118)+4*s(119)+1*s(122)+28*s(123)+1*s(125)+3*s(134)+1
Such that:aux(85) =< V+V1
aux(86) =< V+V1-Out
aux(88) =< V1
aux(89) =< V1-Out
aux(108) =< V
it(26) =< aux(85)
it(27) =< aux(85)
s(121) =< aux(85)
it(26) =< aux(86)
it(27) =< aux(86)
s(121) =< aux(86)
aux(43) =< aux(88)
aux(43) =< aux(89)
aux(59) =< aux(85)
aux(56) =< aux(88)
aux(65) =< aux(85)-1
it(26) =< aux(43)+aux(43)+aux(108)
s(117) =< it(27)*aux(85)
s(116) =< aux(43)+aux(43)+aux(108)
s(135) =< aux(43)+aux(43)+aux(108)
s(120) =< it(27)*aux(59)
s(125) =< it(27)*aux(59)
s(124) =< it(26)*aux(59)
s(115) =< it(26)*aux(56)
s(135) =< it(26)*aux(59)
s(112) =< it(26)*aux(56)
s(122) =< it(26)*aux(65)
s(116) =< it(26)*aux(88)
s(123) =< s(124)
s(114) =< s(115)
s(134) =< s(135)
s(119) =< s(120)
s(118) =< s(121)
s(113) =< s(116)

with precondition: [Out>=2,V>=Out,V1>=Out]

* Chain [[26,27,28,29,30,38],43]: 18*it(26)+13*it(27)+2*s(112)+3*s(113)+8*s(114)+1*s(117)+4*s(119)+1*s(122)+28*s(123)+1*s(125)+3*s(134)+0
Such that:aux(109) =< V
aux(110) =< V+V1
aux(111) =< V1
it(26) =< aux(110)
it(27) =< aux(110)
aux(59) =< aux(110)
aux(56) =< aux(111)
aux(65) =< aux(110)-1
it(26) =< aux(111)+aux(111)+aux(109)
s(117) =< it(27)*aux(110)
s(116) =< aux(111)+aux(111)+aux(109)
s(135) =< aux(111)+aux(111)+aux(109)
s(120) =< it(27)*aux(59)
s(125) =< it(27)*aux(59)
s(124) =< it(26)*aux(59)
s(115) =< it(26)*aux(56)
s(135) =< it(26)*aux(59)
s(112) =< it(26)*aux(56)
s(122) =< it(26)*aux(65)
s(116) =< it(26)*aux(111)
s(123) =< s(124)
s(114) =< s(115)
s(134) =< s(135)
s(119) =< s(120)
s(113) =< s(116)

with precondition: [Out=0,V>=2,V1>=2]

* Chain [[26,27,28,29,30,38],42,45]: 18*it(26)+31*it(27)+2*s(112)+3*s(113)+8*s(114)+1*s(117)+4*s(119)+1*s(122)+28*s(123)+1*s(125)+3*s(134)+5
Such that:aux(112) =< V
aux(113) =< V+V1
aux(114) =< V1
it(27) =< aux(113)
it(26) =< aux(113)
aux(59) =< aux(113)
aux(56) =< aux(114)
aux(65) =< aux(113)-1
it(26) =< aux(114)+aux(114)+aux(112)
s(117) =< it(27)*aux(113)
s(116) =< aux(114)+aux(114)+aux(112)
s(135) =< aux(114)+aux(114)+aux(112)
s(120) =< it(27)*aux(59)
s(125) =< it(27)*aux(59)
s(124) =< it(26)*aux(59)
s(115) =< it(26)*aux(56)
s(135) =< it(26)*aux(59)
s(112) =< it(26)*aux(56)
s(122) =< it(26)*aux(65)
s(116) =< it(26)*aux(114)
s(123) =< s(124)
s(114) =< s(115)
s(134) =< s(135)
s(119) =< s(120)
s(113) =< s(116)

with precondition: [Out=1,V>=2,V1>=2]

* Chain [[26,27,28,29,30,38],42,43]: 18*it(26)+31*it(27)+2*s(112)+3*s(113)+8*s(114)+1*s(117)+4*s(119)+1*s(122)+28*s(123)+1*s(125)+3*s(134)+4
Such that:aux(115) =< V
aux(116) =< V+V1
aux(117) =< V1
it(27) =< aux(116)
it(26) =< aux(116)
aux(59) =< aux(116)
aux(56) =< aux(117)
aux(65) =< aux(116)-1
it(26) =< aux(117)+aux(117)+aux(115)
s(117) =< it(27)*aux(116)
s(116) =< aux(117)+aux(117)+aux(115)
s(135) =< aux(117)+aux(117)+aux(115)
s(120) =< it(27)*aux(59)
s(125) =< it(27)*aux(59)
s(124) =< it(26)*aux(59)
s(115) =< it(26)*aux(56)
s(135) =< it(26)*aux(59)
s(112) =< it(26)*aux(56)
s(122) =< it(26)*aux(65)
s(116) =< it(26)*aux(117)
s(123) =< s(124)
s(114) =< s(115)
s(134) =< s(135)
s(119) =< s(120)
s(113) =< s(116)

with precondition: [Out=0,V>=2,V1>=2]

* Chain [[26,27,28,29,30,38],37,45]: 18*it(26)+13*it(27)+2*s(112)+3*s(113)+8*s(114)+1*s(117)+4*s(119)+1*s(122)+28*s(123)+1*s(125)+3*s(134)+5*s(139)+4*s(142)+5
Such that:aux(84) =< V
aux(87) =< V-Out
aux(120) =< Out
aux(121) =< V+V1
aux(122) =< V1
s(139) =< aux(122)
s(142) =< aux(120)
it(26) =< aux(121)
it(27) =< aux(121)
aux(59) =< aux(121)
aux(56) =< aux(122)
aux(65) =< aux(121)-1
it(26) =< aux(122)+aux(122)+aux(84)
s(117) =< it(27)*aux(121)
it(26) =< aux(122)+aux(122)+aux(87)
s(116) =< aux(122)+aux(122)+aux(87)
s(135) =< aux(122)+aux(122)+aux(87)
s(116) =< aux(122)+aux(122)+aux(84)
s(135) =< aux(122)+aux(122)+aux(84)
s(120) =< it(27)*aux(59)
s(125) =< it(27)*aux(59)
s(124) =< it(26)*aux(59)
s(115) =< it(26)*aux(56)
s(135) =< it(26)*aux(59)
s(112) =< it(26)*aux(56)
s(122) =< it(26)*aux(65)
s(116) =< it(26)*aux(122)
s(123) =< s(124)
s(114) =< s(115)
s(134) =< s(135)
s(119) =< s(120)
s(113) =< s(116)

with precondition: [Out>=2,V>=Out,V1>=Out,V+V1>=2*Out+1]

* Chain [[26,27,28,29,30,38],37,43]: 18*it(26)+13*it(27)+2*s(112)+3*s(113)+8*s(114)+1*s(117)+4*s(119)+1*s(122)+28*s(123)+1*s(125)+3*s(134)+9*s(139)+4
Such that:aux(124) =< V
aux(125) =< V+V1
aux(126) =< V1
s(139) =< aux(126)
it(26) =< aux(125)
it(27) =< aux(125)
aux(59) =< aux(125)
aux(56) =< aux(126)
aux(65) =< aux(125)-1
it(26) =< aux(126)+aux(126)+aux(124)
s(117) =< it(27)*aux(125)
s(116) =< aux(126)+aux(126)+aux(124)
s(135) =< aux(126)+aux(126)+aux(124)
s(120) =< it(27)*aux(59)
s(125) =< it(27)*aux(59)
s(124) =< it(26)*aux(59)
s(115) =< it(26)*aux(56)
s(135) =< it(26)*aux(59)
s(112) =< it(26)*aux(56)
s(122) =< it(26)*aux(65)
s(116) =< it(26)*aux(126)
s(123) =< s(124)
s(114) =< s(115)
s(134) =< s(135)
s(119) =< s(120)
s(113) =< s(116)

with precondition: [Out=0,V>=2,V1>=2,V+V1>=5]

* Chain [[26,27,28,29,30,38],36,[39,41],45]: 18*it(26)+19*it(27)+5*it(39)+2*s(112)+3*s(113)+8*s(114)+1*s(117)+4*s(119)+1*s(122)+28*s(123)+1*s(125)+3*s(134)+6
Such that:aux(13) =< 1
aux(128) =< V
aux(129) =< V+V1
aux(130) =< V1
it(27) =< aux(129)
it(39) =< aux(129)
it(39) =< aux(13)+aux(129)
it(26) =< aux(129)
aux(59) =< aux(129)
aux(56) =< aux(130)
aux(65) =< aux(129)-1
it(26) =< aux(130)+aux(130)+aux(128)
s(117) =< it(27)*aux(129)
s(116) =< aux(130)+aux(130)+aux(128)
s(135) =< aux(130)+aux(130)+aux(128)
s(120) =< it(27)*aux(59)
s(125) =< it(27)*aux(59)
s(124) =< it(26)*aux(59)
s(115) =< it(26)*aux(56)
s(135) =< it(26)*aux(59)
s(112) =< it(26)*aux(56)
s(122) =< it(26)*aux(65)
s(116) =< it(26)*aux(130)
s(123) =< s(124)
s(114) =< s(115)
s(134) =< s(135)
s(119) =< s(120)
s(113) =< s(116)

with precondition: [Out=1,V>=2,V1>=2,V+V1>=5]

* Chain [[26,27,28,29,30,38],36,[39,41],43]: 18*it(26)+19*it(27)+5*it(39)+2*s(112)+3*s(113)+8*s(114)+1*s(117)+4*s(119)+1*s(122)+28*s(123)+1*s(125)+3*s(134)+5
Such that:aux(16) =< 1
aux(132) =< V
aux(133) =< V+V1
aux(134) =< V1
it(27) =< aux(133)
it(39) =< aux(133)
it(39) =< aux(16)+aux(133)
it(26) =< aux(133)
aux(59) =< aux(133)
aux(56) =< aux(134)
aux(65) =< aux(133)-1
it(26) =< aux(134)+aux(134)+aux(132)
s(117) =< it(27)*aux(133)
s(116) =< aux(134)+aux(134)+aux(132)
s(135) =< aux(134)+aux(134)+aux(132)
s(120) =< it(27)*aux(59)
s(125) =< it(27)*aux(59)
s(124) =< it(26)*aux(59)
s(115) =< it(26)*aux(56)
s(135) =< it(26)*aux(59)
s(112) =< it(26)*aux(56)
s(122) =< it(26)*aux(65)
s(116) =< it(26)*aux(134)
s(123) =< s(124)
s(114) =< s(115)
s(134) =< s(135)
s(119) =< s(120)
s(113) =< s(116)

with precondition: [Out=0,V>=2,V1>=2,V+V1>=5]

* Chain [[26,27,28,29,30,38],36,[39,41],42,45]: 18*it(26)+28*it(27)+5*it(39)+9*s(7)+2*s(112)+3*s(113)+8*s(114)+1*s(117)+4*s(119)+1*s(122)+28*s(123)+1*s(125)+3*s(134)+10
Such that:aux(135) =< 1
aux(137) =< V
aux(138) =< V+V1
aux(139) =< V1
it(27) =< aux(138)
s(7) =< aux(135)
it(39) =< aux(138)
it(39) =< aux(135)+aux(138)
it(26) =< aux(138)
aux(59) =< aux(138)
aux(56) =< aux(139)
aux(65) =< aux(138)-1
it(26) =< aux(139)+aux(139)+aux(137)
s(117) =< it(27)*aux(138)
s(116) =< aux(139)+aux(139)+aux(137)
s(135) =< aux(139)+aux(139)+aux(137)
s(120) =< it(27)*aux(59)
s(125) =< it(27)*aux(59)
s(124) =< it(26)*aux(59)
s(115) =< it(26)*aux(56)
s(135) =< it(26)*aux(59)
s(112) =< it(26)*aux(56)
s(122) =< it(26)*aux(65)
s(116) =< it(26)*aux(139)
s(123) =< s(124)
s(114) =< s(115)
s(134) =< s(135)
s(119) =< s(120)
s(113) =< s(116)

with precondition: [Out=1,V>=2,V1>=2,V+V1>=6]

* Chain [[26,27,28,29,30,38],36,[39,41],42,43]: 18*it(26)+28*it(27)+5*it(39)+9*s(7)+2*s(112)+3*s(113)+8*s(114)+1*s(117)+4*s(119)+1*s(122)+28*s(123)+1*s(125)+3*s(134)+9
Such that:aux(140) =< 1
aux(142) =< V
aux(143) =< V+V1
aux(144) =< V1
it(27) =< aux(143)
s(7) =< aux(140)
it(39) =< aux(143)
it(39) =< aux(140)+aux(143)
it(26) =< aux(143)
aux(59) =< aux(143)
aux(56) =< aux(144)
aux(65) =< aux(143)-1
it(26) =< aux(144)+aux(144)+aux(142)
s(117) =< it(27)*aux(143)
s(116) =< aux(144)+aux(144)+aux(142)
s(135) =< aux(144)+aux(144)+aux(142)
s(120) =< it(27)*aux(59)
s(125) =< it(27)*aux(59)
s(124) =< it(26)*aux(59)
s(115) =< it(26)*aux(56)
s(135) =< it(26)*aux(59)
s(112) =< it(26)*aux(56)
s(122) =< it(26)*aux(65)
s(116) =< it(26)*aux(144)
s(123) =< s(124)
s(114) =< s(115)
s(134) =< s(135)
s(119) =< s(120)
s(113) =< s(116)

with precondition: [Out=0,V>=2,V1>=2,V+V1>=6]

* Chain [[26,27,28,29,30,38],36,[39,41],40,45]: 18*it(26)+19*it(27)+5*it(39)+2*s(112)+3*s(113)+8*s(114)+1*s(117)+4*s(119)+1*s(122)+28*s(123)+1*s(125)+3*s(134)+10
Such that:aux(31) =< 1
aux(146) =< V
aux(147) =< V+V1
aux(148) =< V1
it(27) =< aux(147)
it(39) =< aux(147)
it(39) =< aux(31)+aux(147)
it(26) =< aux(147)
aux(59) =< aux(147)
aux(56) =< aux(148)
aux(65) =< aux(147)-1
it(26) =< aux(148)+aux(148)+aux(146)
s(117) =< it(27)*aux(147)
s(116) =< aux(148)+aux(148)+aux(146)
s(135) =< aux(148)+aux(148)+aux(146)
s(120) =< it(27)*aux(59)
s(125) =< it(27)*aux(59)
s(124) =< it(26)*aux(59)
s(115) =< it(26)*aux(56)
s(135) =< it(26)*aux(59)
s(112) =< it(26)*aux(56)
s(122) =< it(26)*aux(65)
s(116) =< it(26)*aux(148)
s(123) =< s(124)
s(114) =< s(115)
s(134) =< s(135)
s(119) =< s(120)
s(113) =< s(116)

with precondition: [Out=1,V>=2,V1>=2,V+V1>=6]

* Chain [[26,27,28,29,30,38],36,[39,41],40,43]: 18*it(26)+19*it(27)+5*it(39)+2*s(112)+3*s(113)+8*s(114)+1*s(117)+4*s(119)+1*s(122)+28*s(123)+1*s(125)+3*s(134)+9
Such that:aux(34) =< 1
aux(150) =< V
aux(151) =< V+V1
aux(152) =< V1
it(27) =< aux(151)
it(39) =< aux(151)
it(39) =< aux(34)+aux(151)
it(26) =< aux(151)
aux(59) =< aux(151)
aux(56) =< aux(152)
aux(65) =< aux(151)-1
it(26) =< aux(152)+aux(152)+aux(150)
s(117) =< it(27)*aux(151)
s(116) =< aux(152)+aux(152)+aux(150)
s(135) =< aux(152)+aux(152)+aux(150)
s(120) =< it(27)*aux(59)
s(125) =< it(27)*aux(59)
s(124) =< it(26)*aux(59)
s(115) =< it(26)*aux(56)
s(135) =< it(26)*aux(59)
s(112) =< it(26)*aux(56)
s(122) =< it(26)*aux(65)
s(116) =< it(26)*aux(152)
s(123) =< s(124)
s(114) =< s(115)
s(134) =< s(135)
s(119) =< s(120)
s(113) =< s(116)

with precondition: [Out=0,V>=2,V1>=2,V+V1>=6]

* Chain [[26,27,28,29,30,38],36,43]: 18*it(26)+13*it(27)+2*s(112)+3*s(113)+8*s(114)+1*s(117)+4*s(119)+1*s(122)+28*s(123)+1*s(125)+3*s(134)+1*s(149)+5
Such that:aux(153) =< V
aux(154) =< V+V1
aux(155) =< V1
s(149) =< aux(155)
it(26) =< aux(154)
it(27) =< aux(154)
aux(59) =< aux(154)
aux(56) =< aux(155)
aux(65) =< aux(154)-1
it(26) =< aux(155)+aux(155)+aux(153)
s(117) =< it(27)*aux(154)
s(116) =< aux(155)+aux(155)+aux(153)
s(135) =< aux(155)+aux(155)+aux(153)
s(120) =< it(27)*aux(59)
s(125) =< it(27)*aux(59)
s(124) =< it(26)*aux(59)
s(115) =< it(26)*aux(56)
s(135) =< it(26)*aux(59)
s(112) =< it(26)*aux(56)
s(122) =< it(26)*aux(65)
s(116) =< it(26)*aux(155)
s(123) =< s(124)
s(114) =< s(115)
s(134) =< s(135)
s(119) =< s(120)
s(113) =< s(116)

with precondition: [Out=0,V>=2,V1>=2,V+V1>=5]

* Chain [[26,27,28,29,30,38],36,42,45]: 18*it(26)+23*it(27)+9*s(7)+2*s(112)+3*s(113)+8*s(114)+1*s(117)+4*s(119)+1*s(122)+28*s(123)+1*s(125)+3*s(134)+10
Such that:aux(22) =< 1
aux(156) =< V
aux(157) =< V+V1
aux(158) =< V1
it(27) =< aux(157)
s(7) =< aux(22)
it(26) =< aux(157)
aux(59) =< aux(157)
aux(56) =< aux(158)
aux(65) =< aux(157)-1
it(26) =< aux(158)+aux(158)+aux(156)
s(117) =< it(27)*aux(157)
s(116) =< aux(158)+aux(158)+aux(156)
s(135) =< aux(158)+aux(158)+aux(156)
s(120) =< it(27)*aux(59)
s(125) =< it(27)*aux(59)
s(124) =< it(26)*aux(59)
s(115) =< it(26)*aux(56)
s(135) =< it(26)*aux(59)
s(112) =< it(26)*aux(56)
s(122) =< it(26)*aux(65)
s(116) =< it(26)*aux(158)
s(123) =< s(124)
s(114) =< s(115)
s(134) =< s(135)
s(119) =< s(120)
s(113) =< s(116)

with precondition: [Out=1,V>=2,V1>=2,V+V1>=5]

* Chain [[26,27,28,29,30,38],36,42,43]: 18*it(26)+23*it(27)+9*s(7)+2*s(112)+3*s(113)+8*s(114)+1*s(117)+4*s(119)+1*s(122)+28*s(123)+1*s(125)+3*s(134)+9
Such that:aux(22) =< 1
aux(159) =< V
aux(160) =< V+V1
aux(161) =< V1
it(27) =< aux(160)
s(7) =< aux(22)
it(26) =< aux(160)
aux(59) =< aux(160)
aux(56) =< aux(161)
aux(65) =< aux(160)-1
it(26) =< aux(161)+aux(161)+aux(159)
s(117) =< it(27)*aux(160)
s(116) =< aux(161)+aux(161)+aux(159)
s(135) =< aux(161)+aux(161)+aux(159)
s(120) =< it(27)*aux(59)
s(125) =< it(27)*aux(59)
s(124) =< it(26)*aux(59)
s(115) =< it(26)*aux(56)
s(135) =< it(26)*aux(59)
s(112) =< it(26)*aux(56)
s(122) =< it(26)*aux(65)
s(116) =< it(26)*aux(161)
s(123) =< s(124)
s(114) =< s(115)
s(134) =< s(135)
s(119) =< s(120)
s(113) =< s(116)

with precondition: [Out=0,V>=2,V1>=2,V+V1>=5]

* Chain [[26,27,28,29,30,38],36,40,45]: 18*it(26)+13*it(27)+2*s(112)+3*s(113)+8*s(114)+1*s(117)+4*s(119)+1*s(122)+28*s(123)+1*s(125)+3*s(134)+1*s(149)+10
Such that:aux(162) =< V
aux(163) =< V+V1
aux(164) =< V1
s(149) =< aux(164)
it(26) =< aux(163)
it(27) =< aux(163)
aux(59) =< aux(163)
aux(56) =< aux(164)
aux(65) =< aux(163)-1
it(26) =< aux(164)+aux(164)+aux(162)
s(117) =< it(27)*aux(163)
s(116) =< aux(164)+aux(164)+aux(162)
s(135) =< aux(164)+aux(164)+aux(162)
s(120) =< it(27)*aux(59)
s(125) =< it(27)*aux(59)
s(124) =< it(26)*aux(59)
s(115) =< it(26)*aux(56)
s(135) =< it(26)*aux(59)
s(112) =< it(26)*aux(56)
s(122) =< it(26)*aux(65)
s(116) =< it(26)*aux(164)
s(123) =< s(124)
s(114) =< s(115)
s(134) =< s(135)
s(119) =< s(120)
s(113) =< s(116)

with precondition: [Out=1,V>=2,V1>=2,V+V1>=5]

* Chain [[26,27,28,29,30,38],36,40,43]: 18*it(26)+13*it(27)+2*s(112)+3*s(113)+8*s(114)+1*s(117)+4*s(119)+1*s(122)+28*s(123)+1*s(125)+3*s(134)+1*s(149)+9
Such that:aux(165) =< V
aux(166) =< V+V1
aux(167) =< V1
s(149) =< aux(167)
it(26) =< aux(166)
it(27) =< aux(166)
aux(59) =< aux(166)
aux(56) =< aux(167)
aux(65) =< aux(166)-1
it(26) =< aux(167)+aux(167)+aux(165)
s(117) =< it(27)*aux(166)
s(116) =< aux(167)+aux(167)+aux(165)
s(135) =< aux(167)+aux(167)+aux(165)
s(120) =< it(27)*aux(59)
s(125) =< it(27)*aux(59)
s(124) =< it(26)*aux(59)
s(115) =< it(26)*aux(56)
s(135) =< it(26)*aux(59)
s(112) =< it(26)*aux(56)
s(122) =< it(26)*aux(65)
s(116) =< it(26)*aux(167)
s(123) =< s(124)
s(114) =< s(115)
s(134) =< s(135)
s(119) =< s(120)
s(113) =< s(116)

with precondition: [Out=0,V>=2,V1>=2,V+V1>=5]

* Chain [[26,27,28,29,30,38],35,[39,41],45]: 18*it(26)+19*it(27)+5*it(39)+2*s(112)+3*s(113)+8*s(114)+1*s(117)+4*s(119)+1*s(122)+28*s(123)+1*s(125)+3*s(134)+6
Such that:aux(13) =< 1
aux(169) =< V
aux(170) =< V+V1
aux(171) =< V1
it(27) =< aux(170)
it(39) =< aux(170)
it(39) =< aux(13)+aux(170)
it(26) =< aux(170)
aux(59) =< aux(170)
aux(56) =< aux(171)
aux(65) =< aux(170)-1
it(26) =< aux(171)+aux(171)+aux(169)
s(117) =< it(27)*aux(170)
s(116) =< aux(171)+aux(171)+aux(169)
s(135) =< aux(171)+aux(171)+aux(169)
s(120) =< it(27)*aux(59)
s(125) =< it(27)*aux(59)
s(124) =< it(26)*aux(59)
s(115) =< it(26)*aux(56)
s(135) =< it(26)*aux(59)
s(112) =< it(26)*aux(56)
s(122) =< it(26)*aux(65)
s(116) =< it(26)*aux(171)
s(123) =< s(124)
s(114) =< s(115)
s(134) =< s(135)
s(119) =< s(120)
s(113) =< s(116)

with precondition: [Out=1,V>=2,V1>=2,V+V1>=5]

* Chain [[26,27,28,29,30,38],35,[39,41],43]: 18*it(26)+19*it(27)+5*it(39)+2*s(112)+3*s(113)+8*s(114)+1*s(117)+4*s(119)+1*s(122)+28*s(123)+1*s(125)+3*s(134)+5
Such that:aux(16) =< 1
aux(173) =< V
aux(174) =< V+V1
aux(175) =< V1
it(27) =< aux(174)
it(39) =< aux(174)
it(39) =< aux(16)+aux(174)
it(26) =< aux(174)
aux(59) =< aux(174)
aux(56) =< aux(175)
aux(65) =< aux(174)-1
it(26) =< aux(175)+aux(175)+aux(173)
s(117) =< it(27)*aux(174)
s(116) =< aux(175)+aux(175)+aux(173)
s(135) =< aux(175)+aux(175)+aux(173)
s(120) =< it(27)*aux(59)
s(125) =< it(27)*aux(59)
s(124) =< it(26)*aux(59)
s(115) =< it(26)*aux(56)
s(135) =< it(26)*aux(59)
s(112) =< it(26)*aux(56)
s(122) =< it(26)*aux(65)
s(116) =< it(26)*aux(175)
s(123) =< s(124)
s(114) =< s(115)
s(134) =< s(135)
s(119) =< s(120)
s(113) =< s(116)

with precondition: [Out=0,V>=2,V1>=2,V+V1>=5]

* Chain [[26,27,28,29,30,38],35,[39,41],42,45]: 18*it(26)+28*it(27)+5*it(39)+9*s(7)+2*s(112)+3*s(113)+8*s(114)+1*s(117)+4*s(119)+1*s(122)+28*s(123)+1*s(125)+3*s(134)+10
Such that:aux(176) =< 1
aux(178) =< V
aux(179) =< V+V1
aux(180) =< V1
it(27) =< aux(179)
s(7) =< aux(176)
it(39) =< aux(179)
it(39) =< aux(176)+aux(179)
it(26) =< aux(179)
aux(59) =< aux(179)
aux(56) =< aux(180)
aux(65) =< aux(179)-1
it(26) =< aux(180)+aux(180)+aux(178)
s(117) =< it(27)*aux(179)
s(116) =< aux(180)+aux(180)+aux(178)
s(135) =< aux(180)+aux(180)+aux(178)
s(120) =< it(27)*aux(59)
s(125) =< it(27)*aux(59)
s(124) =< it(26)*aux(59)
s(115) =< it(26)*aux(56)
s(135) =< it(26)*aux(59)
s(112) =< it(26)*aux(56)
s(122) =< it(26)*aux(65)
s(116) =< it(26)*aux(180)
s(123) =< s(124)
s(114) =< s(115)
s(134) =< s(135)
s(119) =< s(120)
s(113) =< s(116)

with precondition: [Out=1,V>=3,V1>=3]

* Chain [[26,27,28,29,30,38],35,[39,41],42,43]: 18*it(26)+28*it(27)+5*it(39)+9*s(7)+2*s(112)+3*s(113)+8*s(114)+1*s(117)+4*s(119)+1*s(122)+28*s(123)+1*s(125)+3*s(134)+9
Such that:aux(181) =< 1
aux(183) =< V
aux(184) =< V+V1
aux(185) =< V1
it(27) =< aux(184)
s(7) =< aux(181)
it(39) =< aux(184)
it(39) =< aux(181)+aux(184)
it(26) =< aux(184)
aux(59) =< aux(184)
aux(56) =< aux(185)
aux(65) =< aux(184)-1
it(26) =< aux(185)+aux(185)+aux(183)
s(117) =< it(27)*aux(184)
s(116) =< aux(185)+aux(185)+aux(183)
s(135) =< aux(185)+aux(185)+aux(183)
s(120) =< it(27)*aux(59)
s(125) =< it(27)*aux(59)
s(124) =< it(26)*aux(59)
s(115) =< it(26)*aux(56)
s(135) =< it(26)*aux(59)
s(112) =< it(26)*aux(56)
s(122) =< it(26)*aux(65)
s(116) =< it(26)*aux(185)
s(123) =< s(124)
s(114) =< s(115)
s(134) =< s(135)
s(119) =< s(120)
s(113) =< s(116)

with precondition: [Out=0,V>=3,V1>=3]

* Chain [[26,27,28,29,30,38],35,[39,41],40,45]: 18*it(26)+19*it(27)+5*it(39)+2*s(112)+3*s(113)+8*s(114)+1*s(117)+4*s(119)+1*s(122)+28*s(123)+1*s(125)+3*s(134)+10
Such that:aux(31) =< 1
aux(187) =< V
aux(188) =< V+V1
aux(189) =< V1
it(27) =< aux(188)
it(39) =< aux(188)
it(39) =< aux(31)+aux(188)
it(26) =< aux(188)
aux(59) =< aux(188)
aux(56) =< aux(189)
aux(65) =< aux(188)-1
it(26) =< aux(189)+aux(189)+aux(187)
s(117) =< it(27)*aux(188)
s(116) =< aux(189)+aux(189)+aux(187)
s(135) =< aux(189)+aux(189)+aux(187)
s(120) =< it(27)*aux(59)
s(125) =< it(27)*aux(59)
s(124) =< it(26)*aux(59)
s(115) =< it(26)*aux(56)
s(135) =< it(26)*aux(59)
s(112) =< it(26)*aux(56)
s(122) =< it(26)*aux(65)
s(116) =< it(26)*aux(189)
s(123) =< s(124)
s(114) =< s(115)
s(134) =< s(135)
s(119) =< s(120)
s(113) =< s(116)

with precondition: [Out=1,V>=3,V1>=3]

* Chain [[26,27,28,29,30,38],35,[39,41],40,43]: 18*it(26)+19*it(27)+5*it(39)+2*s(112)+3*s(113)+8*s(114)+1*s(117)+4*s(119)+1*s(122)+28*s(123)+1*s(125)+3*s(134)+9
Such that:aux(34) =< 1
aux(191) =< V
aux(192) =< V+V1
aux(193) =< V1
it(27) =< aux(192)
it(39) =< aux(192)
it(39) =< aux(34)+aux(192)
it(26) =< aux(192)
aux(59) =< aux(192)
aux(56) =< aux(193)
aux(65) =< aux(192)-1
it(26) =< aux(193)+aux(193)+aux(191)
s(117) =< it(27)*aux(192)
s(116) =< aux(193)+aux(193)+aux(191)
s(135) =< aux(193)+aux(193)+aux(191)
s(120) =< it(27)*aux(59)
s(125) =< it(27)*aux(59)
s(124) =< it(26)*aux(59)
s(115) =< it(26)*aux(56)
s(135) =< it(26)*aux(59)
s(112) =< it(26)*aux(56)
s(122) =< it(26)*aux(65)
s(116) =< it(26)*aux(193)
s(123) =< s(124)
s(114) =< s(115)
s(134) =< s(135)
s(119) =< s(120)
s(113) =< s(116)

with precondition: [Out=0,V>=3,V1>=3]

* Chain [[26,27,28,29,30,38],35,43]: 18*it(26)+13*it(27)+2*s(112)+3*s(113)+8*s(114)+1*s(117)+4*s(119)+1*s(122)+28*s(123)+1*s(125)+3*s(134)+1*s(150)+5
Such that:aux(194) =< V
aux(195) =< V+V1
aux(196) =< V1
s(150) =< aux(194)
it(26) =< aux(195)
it(27) =< aux(195)
aux(59) =< aux(195)
aux(56) =< aux(196)
aux(65) =< aux(195)-1
it(26) =< aux(196)+aux(196)+aux(194)
s(117) =< it(27)*aux(195)
s(116) =< aux(196)+aux(196)+aux(194)
s(135) =< aux(196)+aux(196)+aux(194)
s(120) =< it(27)*aux(59)
s(125) =< it(27)*aux(59)
s(124) =< it(26)*aux(59)
s(115) =< it(26)*aux(56)
s(135) =< it(26)*aux(59)
s(112) =< it(26)*aux(56)
s(122) =< it(26)*aux(65)
s(116) =< it(26)*aux(196)
s(123) =< s(124)
s(114) =< s(115)
s(134) =< s(135)
s(119) =< s(120)
s(113) =< s(116)

with precondition: [Out=0,V>=2,V1>=2,V+V1>=5]

* Chain [[26,27,28,29,30,38],35,42,45]: 18*it(26)+23*it(27)+9*s(7)+2*s(112)+3*s(113)+8*s(114)+1*s(117)+4*s(119)+1*s(122)+28*s(123)+1*s(125)+3*s(134)+10
Such that:aux(22) =< 1
aux(197) =< V
aux(198) =< V+V1
aux(199) =< V1
it(27) =< aux(198)
s(7) =< aux(22)
it(26) =< aux(198)
aux(59) =< aux(198)
aux(56) =< aux(199)
aux(65) =< aux(198)-1
it(26) =< aux(199)+aux(199)+aux(197)
s(117) =< it(27)*aux(198)
s(116) =< aux(199)+aux(199)+aux(197)
s(135) =< aux(199)+aux(199)+aux(197)
s(120) =< it(27)*aux(59)
s(125) =< it(27)*aux(59)
s(124) =< it(26)*aux(59)
s(115) =< it(26)*aux(56)
s(135) =< it(26)*aux(59)
s(112) =< it(26)*aux(56)
s(122) =< it(26)*aux(65)
s(116) =< it(26)*aux(199)
s(123) =< s(124)
s(114) =< s(115)
s(134) =< s(135)
s(119) =< s(120)
s(113) =< s(116)

with precondition: [Out=1,V>=2,V1>=2,V+V1>=5]

* Chain [[26,27,28,29,30,38],35,42,43]: 18*it(26)+23*it(27)+9*s(7)+2*s(112)+3*s(113)+8*s(114)+1*s(117)+4*s(119)+1*s(122)+28*s(123)+1*s(125)+3*s(134)+9
Such that:aux(22) =< 1
aux(200) =< V
aux(201) =< V+V1
aux(202) =< V1
it(27) =< aux(201)
s(7) =< aux(22)
it(26) =< aux(201)
aux(59) =< aux(201)
aux(56) =< aux(202)
aux(65) =< aux(201)-1
it(26) =< aux(202)+aux(202)+aux(200)
s(117) =< it(27)*aux(201)
s(116) =< aux(202)+aux(202)+aux(200)
s(135) =< aux(202)+aux(202)+aux(200)
s(120) =< it(27)*aux(59)
s(125) =< it(27)*aux(59)
s(124) =< it(26)*aux(59)
s(115) =< it(26)*aux(56)
s(135) =< it(26)*aux(59)
s(112) =< it(26)*aux(56)
s(122) =< it(26)*aux(65)
s(116) =< it(26)*aux(202)
s(123) =< s(124)
s(114) =< s(115)
s(134) =< s(135)
s(119) =< s(120)
s(113) =< s(116)

with precondition: [Out=0,V>=2,V1>=2,V+V1>=5]

* Chain [[26,27,28,29,30,38],35,40,45]: 18*it(26)+13*it(27)+2*s(112)+3*s(113)+8*s(114)+1*s(117)+4*s(119)+1*s(122)+28*s(123)+1*s(125)+3*s(134)+1*s(150)+10
Such that:aux(203) =< V
aux(204) =< V+V1
aux(205) =< V1
s(150) =< aux(203)
it(26) =< aux(204)
it(27) =< aux(204)
aux(59) =< aux(204)
aux(56) =< aux(205)
aux(65) =< aux(204)-1
it(26) =< aux(205)+aux(205)+aux(203)
s(117) =< it(27)*aux(204)
s(116) =< aux(205)+aux(205)+aux(203)
s(135) =< aux(205)+aux(205)+aux(203)
s(120) =< it(27)*aux(59)
s(125) =< it(27)*aux(59)
s(124) =< it(26)*aux(59)
s(115) =< it(26)*aux(56)
s(135) =< it(26)*aux(59)
s(112) =< it(26)*aux(56)
s(122) =< it(26)*aux(65)
s(116) =< it(26)*aux(205)
s(123) =< s(124)
s(114) =< s(115)
s(134) =< s(135)
s(119) =< s(120)
s(113) =< s(116)

with precondition: [Out=1,V>=2,V1>=2,V+V1>=5]

* Chain [[26,27,28,29,30,38],35,40,43]: 18*it(26)+13*it(27)+2*s(112)+3*s(113)+8*s(114)+1*s(117)+4*s(119)+1*s(122)+28*s(123)+1*s(125)+3*s(134)+1*s(150)+9
Such that:aux(206) =< V
aux(207) =< V+V1
aux(208) =< V1
s(150) =< aux(206)
it(26) =< aux(207)
it(27) =< aux(207)
aux(59) =< aux(207)
aux(56) =< aux(208)
aux(65) =< aux(207)-1
it(26) =< aux(208)+aux(208)+aux(206)
s(117) =< it(27)*aux(207)
s(116) =< aux(208)+aux(208)+aux(206)
s(135) =< aux(208)+aux(208)+aux(206)
s(120) =< it(27)*aux(59)
s(125) =< it(27)*aux(59)
s(124) =< it(26)*aux(59)
s(115) =< it(26)*aux(56)
s(135) =< it(26)*aux(59)
s(112) =< it(26)*aux(56)
s(122) =< it(26)*aux(65)
s(116) =< it(26)*aux(208)
s(123) =< s(124)
s(114) =< s(115)
s(134) =< s(135)
s(119) =< s(120)
s(113) =< s(116)

with precondition: [Out=0,V>=2,V1>=2,V+V1>=5]

* Chain [[26,27,28,29,30,38],34,[39,41],45]: 18*it(26)+22*it(27)+5*it(39)+2*s(112)+3*s(113)+8*s(114)+1*s(117)+4*s(119)+1*s(122)+28*s(123)+1*s(125)+3*s(134)+5
Such that:aux(13) =< 1
aux(88) =< V1
aux(89) =< V1+1
aux(211) =< V
aux(212) =< V+V1
it(27) =< aux(212)
it(39) =< aux(212)
it(39) =< aux(13)+aux(212)
it(26) =< aux(212)
aux(43) =< aux(88)
aux(43) =< aux(89)
aux(59) =< aux(212)
aux(56) =< aux(88)
aux(65) =< aux(212)-1
it(26) =< aux(43)+aux(43)+aux(211)
s(117) =< it(27)*aux(212)
s(116) =< aux(43)+aux(43)+aux(211)
s(135) =< aux(43)+aux(43)+aux(211)
s(120) =< it(27)*aux(59)
s(125) =< it(27)*aux(59)
s(124) =< it(26)*aux(59)
s(115) =< it(26)*aux(56)
s(135) =< it(26)*aux(59)
s(112) =< it(26)*aux(56)
s(122) =< it(26)*aux(65)
s(116) =< it(26)*aux(88)
s(123) =< s(124)
s(114) =< s(115)
s(134) =< s(135)
s(119) =< s(120)
s(113) =< s(116)

with precondition: [Out=1,V>=3,V1>=3,V+V1>=7]

* Chain [[26,27,28,29,30,38],34,[39,41],43]: 18*it(26)+22*it(27)+5*it(39)+2*s(112)+3*s(113)+8*s(114)+1*s(117)+4*s(119)+1*s(122)+28*s(123)+1*s(125)+3*s(134)+4
Such that:aux(16) =< 1
aux(88) =< V1
aux(89) =< V1+1
aux(214) =< V
aux(215) =< V+V1
it(27) =< aux(215)
it(39) =< aux(215)
it(39) =< aux(16)+aux(215)
it(26) =< aux(215)
aux(43) =< aux(88)
aux(43) =< aux(89)
aux(59) =< aux(215)
aux(56) =< aux(88)
aux(65) =< aux(215)-1
it(26) =< aux(43)+aux(43)+aux(214)
s(117) =< it(27)*aux(215)
s(116) =< aux(43)+aux(43)+aux(214)
s(135) =< aux(43)+aux(43)+aux(214)
s(120) =< it(27)*aux(59)
s(125) =< it(27)*aux(59)
s(124) =< it(26)*aux(59)
s(115) =< it(26)*aux(56)
s(135) =< it(26)*aux(59)
s(112) =< it(26)*aux(56)
s(122) =< it(26)*aux(65)
s(116) =< it(26)*aux(88)
s(123) =< s(124)
s(114) =< s(115)
s(134) =< s(135)
s(119) =< s(120)
s(113) =< s(116)

with precondition: [Out=0,V>=3,V1>=3,V+V1>=7]

* Chain [[26,27,28,29,30,38],34,[39,41],42,45]: 18*it(26)+31*it(27)+5*it(39)+9*s(7)+2*s(112)+3*s(113)+8*s(114)+1*s(117)+4*s(119)+1*s(122)+28*s(123)+1*s(125)+3*s(134)+9
Such that:aux(216) =< 1
aux(88) =< V1
aux(89) =< V1+1
aux(218) =< V
aux(219) =< V+V1
it(27) =< aux(219)
s(7) =< aux(216)
it(39) =< aux(219)
it(39) =< aux(216)+aux(219)
it(26) =< aux(219)
aux(43) =< aux(88)
aux(43) =< aux(89)
aux(59) =< aux(219)
aux(56) =< aux(88)
aux(65) =< aux(219)-1
it(26) =< aux(43)+aux(43)+aux(218)
s(117) =< it(27)*aux(219)
s(116) =< aux(43)+aux(43)+aux(218)
s(135) =< aux(43)+aux(43)+aux(218)
s(120) =< it(27)*aux(59)
s(125) =< it(27)*aux(59)
s(124) =< it(26)*aux(59)
s(115) =< it(26)*aux(56)
s(135) =< it(26)*aux(59)
s(112) =< it(26)*aux(56)
s(122) =< it(26)*aux(65)
s(116) =< it(26)*aux(88)
s(123) =< s(124)
s(114) =< s(115)
s(134) =< s(135)
s(119) =< s(120)
s(113) =< s(116)

with precondition: [Out=1,V>=4,V1>=4,V+V1>=9]

* Chain [[26,27,28,29,30,38],34,[39,41],42,43]: 18*it(26)+31*it(27)+5*it(39)+9*s(7)+2*s(112)+3*s(113)+8*s(114)+1*s(117)+4*s(119)+1*s(122)+28*s(123)+1*s(125)+3*s(134)+8
Such that:aux(220) =< 1
aux(88) =< V1
aux(89) =< V1+1
aux(222) =< V
aux(223) =< V+V1
it(27) =< aux(223)
s(7) =< aux(220)
it(39) =< aux(223)
it(39) =< aux(220)+aux(223)
it(26) =< aux(223)
aux(43) =< aux(88)
aux(43) =< aux(89)
aux(59) =< aux(223)
aux(56) =< aux(88)
aux(65) =< aux(223)-1
it(26) =< aux(43)+aux(43)+aux(222)
s(117) =< it(27)*aux(223)
s(116) =< aux(43)+aux(43)+aux(222)
s(135) =< aux(43)+aux(43)+aux(222)
s(120) =< it(27)*aux(59)
s(125) =< it(27)*aux(59)
s(124) =< it(26)*aux(59)
s(115) =< it(26)*aux(56)
s(135) =< it(26)*aux(59)
s(112) =< it(26)*aux(56)
s(122) =< it(26)*aux(65)
s(116) =< it(26)*aux(88)
s(123) =< s(124)
s(114) =< s(115)
s(134) =< s(135)
s(119) =< s(120)
s(113) =< s(116)

with precondition: [Out=0,V>=4,V1>=4,V+V1>=9]

* Chain [[26,27,28,29,30,38],34,[39,41],40,45]: 18*it(26)+22*it(27)+5*it(39)+2*s(112)+3*s(113)+8*s(114)+1*s(117)+4*s(119)+1*s(122)+28*s(123)+1*s(125)+3*s(134)+9
Such that:aux(31) =< 1
aux(88) =< V1
aux(89) =< V1+1
aux(225) =< V
aux(226) =< V+V1
it(27) =< aux(226)
it(39) =< aux(226)
it(39) =< aux(31)+aux(226)
it(26) =< aux(226)
aux(43) =< aux(88)
aux(43) =< aux(89)
aux(59) =< aux(226)
aux(56) =< aux(88)
aux(65) =< aux(226)-1
it(26) =< aux(43)+aux(43)+aux(225)
s(117) =< it(27)*aux(226)
s(116) =< aux(43)+aux(43)+aux(225)
s(135) =< aux(43)+aux(43)+aux(225)
s(120) =< it(27)*aux(59)
s(125) =< it(27)*aux(59)
s(124) =< it(26)*aux(59)
s(115) =< it(26)*aux(56)
s(135) =< it(26)*aux(59)
s(112) =< it(26)*aux(56)
s(122) =< it(26)*aux(65)
s(116) =< it(26)*aux(88)
s(123) =< s(124)
s(114) =< s(115)
s(134) =< s(135)
s(119) =< s(120)
s(113) =< s(116)

with precondition: [Out=1,V>=4,V1>=4,V+V1>=9]

* Chain [[26,27,28,29,30,38],34,[39,41],40,43]: 18*it(26)+22*it(27)+5*it(39)+2*s(112)+3*s(113)+8*s(114)+1*s(117)+4*s(119)+1*s(122)+28*s(123)+1*s(125)+3*s(134)+8
Such that:aux(34) =< 1
aux(88) =< V1
aux(89) =< V1+1
aux(228) =< V
aux(229) =< V+V1
it(27) =< aux(229)
it(39) =< aux(229)
it(39) =< aux(34)+aux(229)
it(26) =< aux(229)
aux(43) =< aux(88)
aux(43) =< aux(89)
aux(59) =< aux(229)
aux(56) =< aux(88)
aux(65) =< aux(229)-1
it(26) =< aux(43)+aux(43)+aux(228)
s(117) =< it(27)*aux(229)
s(116) =< aux(43)+aux(43)+aux(228)
s(135) =< aux(43)+aux(43)+aux(228)
s(120) =< it(27)*aux(59)
s(125) =< it(27)*aux(59)
s(124) =< it(26)*aux(59)
s(115) =< it(26)*aux(56)
s(135) =< it(26)*aux(59)
s(112) =< it(26)*aux(56)
s(122) =< it(26)*aux(65)
s(116) =< it(26)*aux(88)
s(123) =< s(124)
s(114) =< s(115)
s(134) =< s(135)
s(119) =< s(120)
s(113) =< s(116)

with precondition: [Out=0,V>=4,V1>=4,V+V1>=9]

* Chain [[26,27,28,29,30,38],34,45]: 18*it(26)+13*it(27)+2*s(112)+3*s(113)+8*s(114)+1*s(117)+4*s(119)+1*s(122)+28*s(123)+1*s(125)+3*s(134)+4*s(151)+5
Such that:aux(231) =< V
aux(232) =< V+V1
aux(233) =< V1
s(151) =< aux(233)
it(26) =< aux(232)
it(27) =< aux(232)
aux(59) =< aux(232)
aux(56) =< aux(233)
aux(65) =< aux(232)-1
it(26) =< aux(233)+aux(233)+aux(231)
s(117) =< it(27)*aux(232)
s(116) =< aux(233)+aux(233)+aux(231)
s(135) =< aux(233)+aux(233)+aux(231)
s(120) =< it(27)*aux(59)
s(125) =< it(27)*aux(59)
s(124) =< it(26)*aux(59)
s(115) =< it(26)*aux(56)
s(135) =< it(26)*aux(59)
s(112) =< it(26)*aux(56)
s(122) =< it(26)*aux(65)
s(116) =< it(26)*aux(233)
s(123) =< s(124)
s(114) =< s(115)
s(134) =< s(135)
s(119) =< s(120)
s(113) =< s(116)

with precondition: [Out=1,V>=2,V1>=2,V+V1>=5]

* Chain [[26,27,28,29,30,38],34,43]: 18*it(26)+13*it(27)+2*s(112)+3*s(113)+8*s(114)+1*s(117)+4*s(119)+1*s(122)+28*s(123)+1*s(125)+3*s(134)+4*s(151)+4
Such that:aux(235) =< V
aux(236) =< V+V1
aux(237) =< V1
s(151) =< aux(237)
it(26) =< aux(236)
it(27) =< aux(236)
aux(59) =< aux(236)
aux(56) =< aux(237)
aux(65) =< aux(236)-1
it(26) =< aux(237)+aux(237)+aux(235)
s(117) =< it(27)*aux(236)
s(116) =< aux(237)+aux(237)+aux(235)
s(135) =< aux(237)+aux(237)+aux(235)
s(120) =< it(27)*aux(59)
s(125) =< it(27)*aux(59)
s(124) =< it(26)*aux(59)
s(115) =< it(26)*aux(56)
s(135) =< it(26)*aux(59)
s(112) =< it(26)*aux(56)
s(122) =< it(26)*aux(65)
s(116) =< it(26)*aux(237)
s(123) =< s(124)
s(114) =< s(115)
s(134) =< s(135)
s(119) =< s(120)
s(113) =< s(116)

with precondition: [Out=0,V>=2,V1>=2,V+V1>=5]

* Chain [[26,27,28,29,30,38],34,42,45]: 18*it(26)+13*it(27)+9*s(7)+13*s(15)+2*s(112)+3*s(113)+8*s(114)+1*s(117)+4*s(119)+1*s(122)+28*s(123)+1*s(125)+3*s(134)+9
Such that:aux(22) =< 1
aux(239) =< V
aux(240) =< V+V1
aux(241) =< V1
s(15) =< aux(241)
s(7) =< aux(22)
it(26) =< aux(240)
it(27) =< aux(240)
aux(59) =< aux(240)
aux(56) =< aux(241)
aux(65) =< aux(240)-1
it(26) =< aux(241)+aux(241)+aux(239)
s(117) =< it(27)*aux(240)
s(116) =< aux(241)+aux(241)+aux(239)
s(135) =< aux(241)+aux(241)+aux(239)
s(120) =< it(27)*aux(59)
s(125) =< it(27)*aux(59)
s(124) =< it(26)*aux(59)
s(115) =< it(26)*aux(56)
s(135) =< it(26)*aux(59)
s(112) =< it(26)*aux(56)
s(122) =< it(26)*aux(65)
s(116) =< it(26)*aux(241)
s(123) =< s(124)
s(114) =< s(115)
s(134) =< s(135)
s(119) =< s(120)
s(113) =< s(116)

with precondition: [Out=1,V>=3,V1>=3,V+V1>=7]

* Chain [[26,27,28,29,30,38],34,42,43]: 18*it(26)+13*it(27)+9*s(7)+13*s(15)+2*s(112)+3*s(113)+8*s(114)+1*s(117)+4*s(119)+1*s(122)+28*s(123)+1*s(125)+3*s(134)+8
Such that:aux(22) =< 1
aux(243) =< V
aux(244) =< V+V1
aux(245) =< V1
s(15) =< aux(245)
s(7) =< aux(22)
it(26) =< aux(244)
it(27) =< aux(244)
aux(59) =< aux(244)
aux(56) =< aux(245)
aux(65) =< aux(244)-1
it(26) =< aux(245)+aux(245)+aux(243)
s(117) =< it(27)*aux(244)
s(116) =< aux(245)+aux(245)+aux(243)
s(135) =< aux(245)+aux(245)+aux(243)
s(120) =< it(27)*aux(59)
s(125) =< it(27)*aux(59)
s(124) =< it(26)*aux(59)
s(115) =< it(26)*aux(56)
s(135) =< it(26)*aux(59)
s(112) =< it(26)*aux(56)
s(122) =< it(26)*aux(65)
s(116) =< it(26)*aux(245)
s(123) =< s(124)
s(114) =< s(115)
s(134) =< s(135)
s(119) =< s(120)
s(113) =< s(116)

with precondition: [Out=0,V>=3,V1>=3,V+V1>=7]

* Chain [[26,27,28,29,30,38],34,40,45]: 18*it(26)+13*it(27)+2*s(112)+3*s(113)+8*s(114)+1*s(117)+4*s(119)+1*s(122)+28*s(123)+1*s(125)+3*s(134)+4*s(151)+9
Such that:aux(247) =< V
aux(248) =< V+V1
aux(249) =< V1
s(151) =< aux(249)
it(26) =< aux(248)
it(27) =< aux(248)
aux(59) =< aux(248)
aux(56) =< aux(249)
aux(65) =< aux(248)-1
it(26) =< aux(249)+aux(249)+aux(247)
s(117) =< it(27)*aux(248)
s(116) =< aux(249)+aux(249)+aux(247)
s(135) =< aux(249)+aux(249)+aux(247)
s(120) =< it(27)*aux(59)
s(125) =< it(27)*aux(59)
s(124) =< it(26)*aux(59)
s(115) =< it(26)*aux(56)
s(135) =< it(26)*aux(59)
s(112) =< it(26)*aux(56)
s(122) =< it(26)*aux(65)
s(116) =< it(26)*aux(249)
s(123) =< s(124)
s(114) =< s(115)
s(134) =< s(135)
s(119) =< s(120)
s(113) =< s(116)

with precondition: [Out=1,V>=3,V1>=3,V+V1>=7]

* Chain [[26,27,28,29,30,38],34,40,43]: 18*it(26)+13*it(27)+2*s(112)+3*s(113)+8*s(114)+1*s(117)+4*s(119)+1*s(122)+28*s(123)+1*s(125)+3*s(134)+4*s(151)+8
Such that:aux(251) =< V
aux(252) =< V+V1
aux(253) =< V1
s(151) =< aux(253)
it(26) =< aux(252)
it(27) =< aux(252)
aux(59) =< aux(252)
aux(56) =< aux(253)
aux(65) =< aux(252)-1
it(26) =< aux(253)+aux(253)+aux(251)
s(117) =< it(27)*aux(252)
s(116) =< aux(253)+aux(253)+aux(251)
s(135) =< aux(253)+aux(253)+aux(251)
s(120) =< it(27)*aux(59)
s(125) =< it(27)*aux(59)
s(124) =< it(26)*aux(59)
s(115) =< it(26)*aux(56)
s(135) =< it(26)*aux(59)
s(112) =< it(26)*aux(56)
s(122) =< it(26)*aux(65)
s(116) =< it(26)*aux(253)
s(123) =< s(124)
s(114) =< s(115)
s(134) =< s(135)
s(119) =< s(120)
s(113) =< s(116)

with precondition: [Out=0,V>=3,V1>=3,V+V1>=7]

* Chain [[26,27,28,29,30,38],33,[39,41],45]: 18*it(26)+19*it(27)+5*it(39)+2*s(112)+3*s(113)+8*s(114)+1*s(117)+4*s(119)+1*s(122)+28*s(123)+1*s(125)+3*s(134)+5
Such that:aux(13) =< 1
aux(255) =< V
aux(256) =< V+V1
aux(257) =< V1
it(27) =< aux(256)
it(39) =< aux(256)
it(39) =< aux(13)+aux(256)
it(26) =< aux(256)
aux(59) =< aux(256)
aux(56) =< aux(257)
aux(65) =< aux(256)-1
it(26) =< aux(257)+aux(257)+aux(255)
s(117) =< it(27)*aux(256)
s(116) =< aux(257)+aux(257)+aux(255)
s(135) =< aux(257)+aux(257)+aux(255)
s(120) =< it(27)*aux(59)
s(125) =< it(27)*aux(59)
s(124) =< it(26)*aux(59)
s(115) =< it(26)*aux(56)
s(135) =< it(26)*aux(59)
s(112) =< it(26)*aux(56)
s(122) =< it(26)*aux(65)
s(116) =< it(26)*aux(257)
s(123) =< s(124)
s(114) =< s(115)
s(134) =< s(135)
s(119) =< s(120)
s(113) =< s(116)

with precondition: [Out=1,V>=2,V1>=2,V+V1>=5]

* Chain [[26,27,28,29,30,38],33,[39,41],43]: 18*it(26)+19*it(27)+5*it(39)+2*s(112)+3*s(113)+8*s(114)+1*s(117)+4*s(119)+1*s(122)+28*s(123)+1*s(125)+3*s(134)+4
Such that:aux(16) =< 1
aux(259) =< V
aux(260) =< V+V1
aux(261) =< V1
it(27) =< aux(260)
it(39) =< aux(260)
it(39) =< aux(16)+aux(260)
it(26) =< aux(260)
aux(59) =< aux(260)
aux(56) =< aux(261)
aux(65) =< aux(260)-1
it(26) =< aux(261)+aux(261)+aux(259)
s(117) =< it(27)*aux(260)
s(116) =< aux(261)+aux(261)+aux(259)
s(135) =< aux(261)+aux(261)+aux(259)
s(120) =< it(27)*aux(59)
s(125) =< it(27)*aux(59)
s(124) =< it(26)*aux(59)
s(115) =< it(26)*aux(56)
s(135) =< it(26)*aux(59)
s(112) =< it(26)*aux(56)
s(122) =< it(26)*aux(65)
s(116) =< it(26)*aux(261)
s(123) =< s(124)
s(114) =< s(115)
s(134) =< s(135)
s(119) =< s(120)
s(113) =< s(116)

with precondition: [Out=0,V>=2,V1>=2,V+V1>=5]

* Chain [[26,27,28,29,30,38],33,[39,41],42,45]: 18*it(26)+28*it(27)+5*it(39)+9*s(7)+2*s(112)+3*s(113)+8*s(114)+1*s(117)+4*s(119)+1*s(122)+28*s(123)+1*s(125)+3*s(134)+9
Such that:aux(262) =< 1
aux(264) =< V
aux(265) =< V+V1
aux(266) =< V1
it(27) =< aux(265)
s(7) =< aux(262)
it(39) =< aux(265)
it(39) =< aux(262)+aux(265)
it(26) =< aux(265)
aux(59) =< aux(265)
aux(56) =< aux(266)
aux(65) =< aux(265)-1
it(26) =< aux(266)+aux(266)+aux(264)
s(117) =< it(27)*aux(265)
s(116) =< aux(266)+aux(266)+aux(264)
s(135) =< aux(266)+aux(266)+aux(264)
s(120) =< it(27)*aux(59)
s(125) =< it(27)*aux(59)
s(124) =< it(26)*aux(59)
s(115) =< it(26)*aux(56)
s(135) =< it(26)*aux(59)
s(112) =< it(26)*aux(56)
s(122) =< it(26)*aux(65)
s(116) =< it(26)*aux(266)
s(123) =< s(124)
s(114) =< s(115)
s(134) =< s(135)
s(119) =< s(120)
s(113) =< s(116)

with precondition: [Out=1,V>=3,V1>=3,V+V1>=7]

* Chain [[26,27,28,29,30,38],33,[39,41],42,43]: 18*it(26)+28*it(27)+5*it(39)+9*s(7)+2*s(112)+3*s(113)+8*s(114)+1*s(117)+4*s(119)+1*s(122)+28*s(123)+1*s(125)+3*s(134)+8
Such that:aux(267) =< 1
aux(269) =< V
aux(270) =< V+V1
aux(271) =< V1
it(27) =< aux(270)
s(7) =< aux(267)
it(39) =< aux(270)
it(39) =< aux(267)+aux(270)
it(26) =< aux(270)
aux(59) =< aux(270)
aux(56) =< aux(271)
aux(65) =< aux(270)-1
it(26) =< aux(271)+aux(271)+aux(269)
s(117) =< it(27)*aux(270)
s(116) =< aux(271)+aux(271)+aux(269)
s(135) =< aux(271)+aux(271)+aux(269)
s(120) =< it(27)*aux(59)
s(125) =< it(27)*aux(59)
s(124) =< it(26)*aux(59)
s(115) =< it(26)*aux(56)
s(135) =< it(26)*aux(59)
s(112) =< it(26)*aux(56)
s(122) =< it(26)*aux(65)
s(116) =< it(26)*aux(271)
s(123) =< s(124)
s(114) =< s(115)
s(134) =< s(135)
s(119) =< s(120)
s(113) =< s(116)

with precondition: [Out=0,V>=3,V1>=3,V+V1>=7]

* Chain [[26,27,28,29,30,38],33,[39,41],40,45]: 18*it(26)+19*it(27)+5*it(39)+2*s(112)+3*s(113)+8*s(114)+1*s(117)+4*s(119)+1*s(122)+28*s(123)+1*s(125)+3*s(134)+9
Such that:aux(31) =< 1
aux(273) =< V
aux(274) =< V+V1
aux(275) =< V1
it(27) =< aux(274)
it(39) =< aux(274)
it(39) =< aux(31)+aux(274)
it(26) =< aux(274)
aux(59) =< aux(274)
aux(56) =< aux(275)
aux(65) =< aux(274)-1
it(26) =< aux(275)+aux(275)+aux(273)
s(117) =< it(27)*aux(274)
s(116) =< aux(275)+aux(275)+aux(273)
s(135) =< aux(275)+aux(275)+aux(273)
s(120) =< it(27)*aux(59)
s(125) =< it(27)*aux(59)
s(124) =< it(26)*aux(59)
s(115) =< it(26)*aux(56)
s(135) =< it(26)*aux(59)
s(112) =< it(26)*aux(56)
s(122) =< it(26)*aux(65)
s(116) =< it(26)*aux(275)
s(123) =< s(124)
s(114) =< s(115)
s(134) =< s(135)
s(119) =< s(120)
s(113) =< s(116)

with precondition: [Out=1,V>=3,V1>=3,V+V1>=7]

* Chain [[26,27,28,29,30,38],33,[39,41],40,43]: 18*it(26)+19*it(27)+5*it(39)+2*s(112)+3*s(113)+8*s(114)+1*s(117)+4*s(119)+1*s(122)+28*s(123)+1*s(125)+3*s(134)+8
Such that:aux(34) =< 1
aux(277) =< V
aux(278) =< V+V1
aux(279) =< V1
it(27) =< aux(278)
it(39) =< aux(278)
it(39) =< aux(34)+aux(278)
it(26) =< aux(278)
aux(59) =< aux(278)
aux(56) =< aux(279)
aux(65) =< aux(278)-1
it(26) =< aux(279)+aux(279)+aux(277)
s(117) =< it(27)*aux(278)
s(116) =< aux(279)+aux(279)+aux(277)
s(135) =< aux(279)+aux(279)+aux(277)
s(120) =< it(27)*aux(59)
s(125) =< it(27)*aux(59)
s(124) =< it(26)*aux(59)
s(115) =< it(26)*aux(56)
s(135) =< it(26)*aux(59)
s(112) =< it(26)*aux(56)
s(122) =< it(26)*aux(65)
s(116) =< it(26)*aux(279)
s(123) =< s(124)
s(114) =< s(115)
s(134) =< s(135)
s(119) =< s(120)
s(113) =< s(116)

with precondition: [Out=0,V>=3,V1>=3,V+V1>=7]

* Chain [[26,27,28,29,30,38],33,43]: 18*it(26)+13*it(27)+2*s(112)+3*s(113)+8*s(114)+1*s(117)+4*s(119)+1*s(122)+28*s(123)+1*s(125)+3*s(134)+1*s(155)+4
Such that:aux(280) =< V
aux(281) =< V+V1
aux(282) =< V1
s(155) =< aux(282)
it(26) =< aux(281)
it(27) =< aux(281)
aux(59) =< aux(281)
aux(56) =< aux(282)
aux(65) =< aux(281)-1
it(26) =< aux(282)+aux(282)+aux(280)
s(117) =< it(27)*aux(281)
s(116) =< aux(282)+aux(282)+aux(280)
s(135) =< aux(282)+aux(282)+aux(280)
s(120) =< it(27)*aux(59)
s(125) =< it(27)*aux(59)
s(124) =< it(26)*aux(59)
s(115) =< it(26)*aux(56)
s(135) =< it(26)*aux(59)
s(112) =< it(26)*aux(56)
s(122) =< it(26)*aux(65)
s(116) =< it(26)*aux(282)
s(123) =< s(124)
s(114) =< s(115)
s(134) =< s(135)
s(119) =< s(120)
s(113) =< s(116)

with precondition: [Out=0,V>=2,V1>=2,V+V1>=5]

* Chain [[26,27,28,29,30,38],33,42,45]: 18*it(26)+23*it(27)+9*s(7)+2*s(112)+3*s(113)+8*s(114)+1*s(117)+4*s(119)+1*s(122)+28*s(123)+1*s(125)+3*s(134)+9
Such that:aux(22) =< 1
aux(284) =< V
aux(285) =< V+V1
aux(286) =< V1
it(27) =< aux(285)
s(7) =< aux(22)
it(26) =< aux(285)
aux(59) =< aux(285)
aux(56) =< aux(286)
aux(65) =< aux(285)-1
it(26) =< aux(286)+aux(286)+aux(284)
s(117) =< it(27)*aux(285)
s(116) =< aux(286)+aux(286)+aux(284)
s(135) =< aux(286)+aux(286)+aux(284)
s(120) =< it(27)*aux(59)
s(125) =< it(27)*aux(59)
s(124) =< it(26)*aux(59)
s(115) =< it(26)*aux(56)
s(135) =< it(26)*aux(59)
s(112) =< it(26)*aux(56)
s(122) =< it(26)*aux(65)
s(116) =< it(26)*aux(286)
s(123) =< s(124)
s(114) =< s(115)
s(134) =< s(135)
s(119) =< s(120)
s(113) =< s(116)

with precondition: [Out=1,V>=2,V1>=2,V+V1>=5]

* Chain [[26,27,28,29,30,38],33,42,43]: 18*it(26)+23*it(27)+9*s(7)+2*s(112)+3*s(113)+8*s(114)+1*s(117)+4*s(119)+1*s(122)+28*s(123)+1*s(125)+3*s(134)+8
Such that:aux(22) =< 1
aux(288) =< V
aux(289) =< V+V1
aux(290) =< V1
it(27) =< aux(289)
s(7) =< aux(22)
it(26) =< aux(289)
aux(59) =< aux(289)
aux(56) =< aux(290)
aux(65) =< aux(289)-1
it(26) =< aux(290)+aux(290)+aux(288)
s(117) =< it(27)*aux(289)
s(116) =< aux(290)+aux(290)+aux(288)
s(135) =< aux(290)+aux(290)+aux(288)
s(120) =< it(27)*aux(59)
s(125) =< it(27)*aux(59)
s(124) =< it(26)*aux(59)
s(115) =< it(26)*aux(56)
s(135) =< it(26)*aux(59)
s(112) =< it(26)*aux(56)
s(122) =< it(26)*aux(65)
s(116) =< it(26)*aux(290)
s(123) =< s(124)
s(114) =< s(115)
s(134) =< s(135)
s(119) =< s(120)
s(113) =< s(116)

with precondition: [Out=0,V>=2,V1>=2,V+V1>=5]

* Chain [[26,27,28,29,30,38],33,40,45]: 18*it(26)+13*it(27)+2*s(112)+3*s(113)+8*s(114)+1*s(117)+4*s(119)+1*s(122)+28*s(123)+1*s(125)+3*s(134)+1*s(155)+9
Such that:aux(291) =< V
aux(292) =< V+V1
aux(293) =< V1
s(155) =< aux(293)
it(26) =< aux(292)
it(27) =< aux(292)
aux(59) =< aux(292)
aux(56) =< aux(293)
aux(65) =< aux(292)-1
it(26) =< aux(293)+aux(293)+aux(291)
s(117) =< it(27)*aux(292)
s(116) =< aux(293)+aux(293)+aux(291)
s(135) =< aux(293)+aux(293)+aux(291)
s(120) =< it(27)*aux(59)
s(125) =< it(27)*aux(59)
s(124) =< it(26)*aux(59)
s(115) =< it(26)*aux(56)
s(135) =< it(26)*aux(59)
s(112) =< it(26)*aux(56)
s(122) =< it(26)*aux(65)
s(116) =< it(26)*aux(293)
s(123) =< s(124)
s(114) =< s(115)
s(134) =< s(135)
s(119) =< s(120)
s(113) =< s(116)

with precondition: [Out=1,V>=2,V1>=2,V+V1>=5]

* Chain [[26,27,28,29,30,38],33,40,43]: 18*it(26)+13*it(27)+2*s(112)+3*s(113)+8*s(114)+1*s(117)+4*s(119)+1*s(122)+28*s(123)+1*s(125)+3*s(134)+1*s(155)+8
Such that:aux(294) =< V
aux(295) =< V+V1
aux(296) =< V1
s(155) =< aux(296)
it(26) =< aux(295)
it(27) =< aux(295)
aux(59) =< aux(295)
aux(56) =< aux(296)
aux(65) =< aux(295)-1
it(26) =< aux(296)+aux(296)+aux(294)
s(117) =< it(27)*aux(295)
s(116) =< aux(296)+aux(296)+aux(294)
s(135) =< aux(296)+aux(296)+aux(294)
s(120) =< it(27)*aux(59)
s(125) =< it(27)*aux(59)
s(124) =< it(26)*aux(59)
s(115) =< it(26)*aux(56)
s(135) =< it(26)*aux(59)
s(112) =< it(26)*aux(56)
s(122) =< it(26)*aux(65)
s(116) =< it(26)*aux(296)
s(123) =< s(124)
s(114) =< s(115)
s(134) =< s(135)
s(119) =< s(120)
s(113) =< s(116)

with precondition: [Out=0,V>=2,V1>=2,V+V1>=5]

* Chain [[26,27,28,29,30,38],32,[39,41],45]: 18*it(26)+10*it(27)+5*it(39)+9*it(41)+2*s(112)+3*s(113)+8*s(114)+1*s(117)+3*s(118)+4*s(119)+1*s(122)+28*s(123)+1*s(125)+3*s(134)+6
Such that:aux(13) =< 1
aux(88) =< V1
aux(89) =< V1+1
aux(299) =< V
aux(300) =< V+V1
aux(301) =< V+V1+1
it(41) =< aux(301)
it(39) =< aux(301)
it(39) =< aux(13)+aux(300)
it(26) =< aux(300)
it(27) =< aux(300)
s(121) =< aux(300)
it(26) =< aux(301)
it(27) =< aux(301)
s(121) =< aux(301)
aux(43) =< aux(88)
aux(43) =< aux(89)
aux(59) =< aux(300)
aux(56) =< aux(88)
aux(65) =< aux(300)-1
it(26) =< aux(43)+aux(43)+aux(299)
s(117) =< it(27)*aux(300)
s(116) =< aux(43)+aux(43)+aux(299)
s(135) =< aux(43)+aux(43)+aux(299)
s(120) =< it(27)*aux(59)
s(125) =< it(27)*aux(59)
s(124) =< it(26)*aux(59)
s(115) =< it(26)*aux(56)
s(135) =< it(26)*aux(59)
s(112) =< it(26)*aux(56)
s(122) =< it(26)*aux(65)
s(116) =< it(26)*aux(88)
s(123) =< s(124)
s(114) =< s(115)
s(134) =< s(135)
s(119) =< s(120)
s(118) =< s(121)
s(113) =< s(116)

with precondition: [Out=1,V>=3,V1>=3]

* Chain [[26,27,28,29,30,38],32,[39,41],43]: 18*it(26)+10*it(27)+5*it(39)+9*it(41)+2*s(112)+3*s(113)+8*s(114)+1*s(117)+3*s(118)+4*s(119)+1*s(122)+28*s(123)+1*s(125)+3*s(134)+5
Such that:aux(16) =< 1
aux(88) =< V1
aux(89) =< V1+1
aux(303) =< V
aux(304) =< V+V1
aux(305) =< V+V1+1
it(41) =< aux(305)
it(39) =< aux(305)
it(39) =< aux(16)+aux(304)
it(26) =< aux(304)
it(27) =< aux(304)
s(121) =< aux(304)
it(26) =< aux(305)
it(27) =< aux(305)
s(121) =< aux(305)
aux(43) =< aux(88)
aux(43) =< aux(89)
aux(59) =< aux(304)
aux(56) =< aux(88)
aux(65) =< aux(304)-1
it(26) =< aux(43)+aux(43)+aux(303)
s(117) =< it(27)*aux(304)
s(116) =< aux(43)+aux(43)+aux(303)
s(135) =< aux(43)+aux(43)+aux(303)
s(120) =< it(27)*aux(59)
s(125) =< it(27)*aux(59)
s(124) =< it(26)*aux(59)
s(115) =< it(26)*aux(56)
s(135) =< it(26)*aux(59)
s(112) =< it(26)*aux(56)
s(122) =< it(26)*aux(65)
s(116) =< it(26)*aux(88)
s(123) =< s(124)
s(114) =< s(115)
s(134) =< s(135)
s(119) =< s(120)
s(118) =< s(121)
s(113) =< s(116)

with precondition: [Out=0,V>=3,V1>=3]

* Chain [[26,27,28,29,30,38],32,[39,41],42,45]: 18*it(26)+10*it(27)+5*it(39)+18*it(41)+9*s(7)+2*s(112)+3*s(113)+8*s(114)+1*s(117)+3*s(118)+4*s(119)+1*s(122)+28*s(123)+1*s(125)+3*s(134)+10
Such that:aux(306) =< 1
aux(88) =< V1
aux(89) =< V1+1
aux(308) =< V
aux(309) =< V+V1
aux(310) =< V+V1+1
it(41) =< aux(310)
s(7) =< aux(306)
it(39) =< aux(310)
it(39) =< aux(306)+aux(309)
it(26) =< aux(309)
it(27) =< aux(309)
s(121) =< aux(309)
it(26) =< aux(310)
it(27) =< aux(310)
s(121) =< aux(310)
aux(43) =< aux(88)
aux(43) =< aux(89)
aux(59) =< aux(309)
aux(56) =< aux(88)
aux(65) =< aux(309)-1
it(26) =< aux(43)+aux(43)+aux(308)
s(117) =< it(27)*aux(309)
s(116) =< aux(43)+aux(43)+aux(308)
s(135) =< aux(43)+aux(43)+aux(308)
s(120) =< it(27)*aux(59)
s(125) =< it(27)*aux(59)
s(124) =< it(26)*aux(59)
s(115) =< it(26)*aux(56)
s(135) =< it(26)*aux(59)
s(112) =< it(26)*aux(56)
s(122) =< it(26)*aux(65)
s(116) =< it(26)*aux(88)
s(123) =< s(124)
s(114) =< s(115)
s(134) =< s(135)
s(119) =< s(120)
s(118) =< s(121)
s(113) =< s(116)

with precondition: [Out=1,V>=4,V1>=4]

* Chain [[26,27,28,29,30,38],32,[39,41],42,43]: 18*it(26)+10*it(27)+5*it(39)+18*it(41)+9*s(7)+2*s(112)+3*s(113)+8*s(114)+1*s(117)+3*s(118)+4*s(119)+1*s(122)+28*s(123)+1*s(125)+3*s(134)+9
Such that:aux(311) =< 1
aux(88) =< V1
aux(89) =< V1+1
aux(313) =< V
aux(314) =< V+V1
aux(315) =< V+V1+1
it(41) =< aux(315)
s(7) =< aux(311)
it(39) =< aux(315)
it(39) =< aux(311)+aux(314)
it(26) =< aux(314)
it(27) =< aux(314)
s(121) =< aux(314)
it(26) =< aux(315)
it(27) =< aux(315)
s(121) =< aux(315)
aux(43) =< aux(88)
aux(43) =< aux(89)
aux(59) =< aux(314)
aux(56) =< aux(88)
aux(65) =< aux(314)-1
it(26) =< aux(43)+aux(43)+aux(313)
s(117) =< it(27)*aux(314)
s(116) =< aux(43)+aux(43)+aux(313)
s(135) =< aux(43)+aux(43)+aux(313)
s(120) =< it(27)*aux(59)
s(125) =< it(27)*aux(59)
s(124) =< it(26)*aux(59)
s(115) =< it(26)*aux(56)
s(135) =< it(26)*aux(59)
s(112) =< it(26)*aux(56)
s(122) =< it(26)*aux(65)
s(116) =< it(26)*aux(88)
s(123) =< s(124)
s(114) =< s(115)
s(134) =< s(135)
s(119) =< s(120)
s(118) =< s(121)
s(113) =< s(116)

with precondition: [Out=0,V>=4,V1>=4]

* Chain [[26,27,28,29,30,38],32,[39,41],40,45]: 18*it(26)+10*it(27)+5*it(39)+9*it(41)+2*s(112)+3*s(113)+8*s(114)+1*s(117)+3*s(118)+4*s(119)+1*s(122)+28*s(123)+1*s(125)+3*s(134)+10
Such that:aux(31) =< 1
aux(88) =< V1
aux(89) =< V1+1
aux(317) =< V
aux(318) =< V+V1
aux(319) =< V+V1+1
it(41) =< aux(319)
it(39) =< aux(319)
it(39) =< aux(31)+aux(318)
it(26) =< aux(318)
it(27) =< aux(318)
s(121) =< aux(318)
it(26) =< aux(319)
it(27) =< aux(319)
s(121) =< aux(319)
aux(43) =< aux(88)
aux(43) =< aux(89)
aux(59) =< aux(318)
aux(56) =< aux(88)
aux(65) =< aux(318)-1
it(26) =< aux(43)+aux(43)+aux(317)
s(117) =< it(27)*aux(318)
s(116) =< aux(43)+aux(43)+aux(317)
s(135) =< aux(43)+aux(43)+aux(317)
s(120) =< it(27)*aux(59)
s(125) =< it(27)*aux(59)
s(124) =< it(26)*aux(59)
s(115) =< it(26)*aux(56)
s(135) =< it(26)*aux(59)
s(112) =< it(26)*aux(56)
s(122) =< it(26)*aux(65)
s(116) =< it(26)*aux(88)
s(123) =< s(124)
s(114) =< s(115)
s(134) =< s(135)
s(119) =< s(120)
s(118) =< s(121)
s(113) =< s(116)

with precondition: [Out=1,V>=4,V1>=4]

* Chain [[26,27,28,29,30,38],32,[39,41],40,43]: 18*it(26)+10*it(27)+5*it(39)+9*it(41)+2*s(112)+3*s(113)+8*s(114)+1*s(117)+3*s(118)+4*s(119)+1*s(122)+28*s(123)+1*s(125)+3*s(134)+9
Such that:aux(34) =< 1
aux(88) =< V1
aux(89) =< V1+1
aux(321) =< V
aux(322) =< V+V1
aux(323) =< V+V1+1
it(41) =< aux(323)
it(39) =< aux(323)
it(39) =< aux(34)+aux(322)
it(26) =< aux(322)
it(27) =< aux(322)
s(121) =< aux(322)
it(26) =< aux(323)
it(27) =< aux(323)
s(121) =< aux(323)
aux(43) =< aux(88)
aux(43) =< aux(89)
aux(59) =< aux(322)
aux(56) =< aux(88)
aux(65) =< aux(322)-1
it(26) =< aux(43)+aux(43)+aux(321)
s(117) =< it(27)*aux(322)
s(116) =< aux(43)+aux(43)+aux(321)
s(135) =< aux(43)+aux(43)+aux(321)
s(120) =< it(27)*aux(59)
s(125) =< it(27)*aux(59)
s(124) =< it(26)*aux(59)
s(115) =< it(26)*aux(56)
s(135) =< it(26)*aux(59)
s(112) =< it(26)*aux(56)
s(122) =< it(26)*aux(65)
s(116) =< it(26)*aux(88)
s(123) =< s(124)
s(114) =< s(115)
s(134) =< s(135)
s(119) =< s(120)
s(118) =< s(121)
s(113) =< s(116)

with precondition: [Out=0,V>=4,V1>=4]

* Chain [[26,27,28,29,30,38],32,45]: 18*it(26)+13*it(27)+2*s(112)+3*s(113)+8*s(114)+1*s(117)+4*s(119)+1*s(122)+28*s(123)+1*s(125)+3*s(134)+4*s(156)+6
Such that:aux(325) =< V
aux(326) =< V+V1
aux(327) =< V1
s(156) =< aux(327)
it(26) =< aux(326)
it(27) =< aux(326)
aux(59) =< aux(326)
aux(56) =< aux(327)
aux(65) =< aux(326)-1
it(26) =< aux(327)+aux(327)+aux(325)
s(117) =< it(27)*aux(326)
s(116) =< aux(327)+aux(327)+aux(325)
s(135) =< aux(327)+aux(327)+aux(325)
s(120) =< it(27)*aux(59)
s(125) =< it(27)*aux(59)
s(124) =< it(26)*aux(59)
s(115) =< it(26)*aux(56)
s(135) =< it(26)*aux(59)
s(112) =< it(26)*aux(56)
s(122) =< it(26)*aux(65)
s(116) =< it(26)*aux(327)
s(123) =< s(124)
s(114) =< s(115)
s(134) =< s(135)
s(119) =< s(120)
s(113) =< s(116)

with precondition: [Out=1,V>=2,V1>=2,V+V1>=5]

* Chain [[26,27,28,29,30,38],32,43]: 18*it(26)+13*it(27)+2*s(112)+3*s(113)+8*s(114)+1*s(117)+4*s(119)+1*s(122)+28*s(123)+1*s(125)+3*s(134)+4*s(156)+5
Such that:aux(329) =< V
aux(330) =< V+V1
aux(331) =< V1
s(156) =< aux(329)
it(26) =< aux(330)
it(27) =< aux(330)
aux(59) =< aux(330)
aux(56) =< aux(331)
aux(65) =< aux(330)-1
it(26) =< aux(331)+aux(331)+aux(329)
s(117) =< it(27)*aux(330)
s(116) =< aux(331)+aux(331)+aux(329)
s(135) =< aux(331)+aux(331)+aux(329)
s(120) =< it(27)*aux(59)
s(125) =< it(27)*aux(59)
s(124) =< it(26)*aux(59)
s(115) =< it(26)*aux(56)
s(135) =< it(26)*aux(59)
s(112) =< it(26)*aux(56)
s(122) =< it(26)*aux(65)
s(116) =< it(26)*aux(331)
s(123) =< s(124)
s(114) =< s(115)
s(134) =< s(135)
s(119) =< s(120)
s(113) =< s(116)

with precondition: [Out=0,V>=2,V1>=2,V+V1>=5]

* Chain [[26,27,28,29,30,38],32,42,45]: 18*it(26)+26*it(27)+9*s(7)+2*s(112)+3*s(113)+8*s(114)+1*s(117)+4*s(119)+1*s(122)+28*s(123)+1*s(125)+3*s(134)+10
Such that:aux(22) =< 1
aux(333) =< V
aux(334) =< V+V1
aux(335) =< V1
it(27) =< aux(334)
s(7) =< aux(22)
it(26) =< aux(334)
aux(59) =< aux(334)
aux(56) =< aux(335)
aux(65) =< aux(334)-1
it(26) =< aux(335)+aux(335)+aux(333)
s(117) =< it(27)*aux(334)
s(116) =< aux(335)+aux(335)+aux(333)
s(135) =< aux(335)+aux(335)+aux(333)
s(120) =< it(27)*aux(59)
s(125) =< it(27)*aux(59)
s(124) =< it(26)*aux(59)
s(115) =< it(26)*aux(56)
s(135) =< it(26)*aux(59)
s(112) =< it(26)*aux(56)
s(122) =< it(26)*aux(65)
s(116) =< it(26)*aux(335)
s(123) =< s(124)
s(114) =< s(115)
s(134) =< s(135)
s(119) =< s(120)
s(113) =< s(116)

with precondition: [Out=1,V>=3,V1>=3]

* Chain [[26,27,28,29,30,38],32,42,43]: 18*it(26)+26*it(27)+9*s(7)+2*s(112)+3*s(113)+8*s(114)+1*s(117)+4*s(119)+1*s(122)+28*s(123)+1*s(125)+3*s(134)+9
Such that:aux(22) =< 1
aux(337) =< V
aux(338) =< V+V1
aux(339) =< V1
it(27) =< aux(338)
s(7) =< aux(22)
it(26) =< aux(338)
aux(59) =< aux(338)
aux(56) =< aux(339)
aux(65) =< aux(338)-1
it(26) =< aux(339)+aux(339)+aux(337)
s(117) =< it(27)*aux(338)
s(116) =< aux(339)+aux(339)+aux(337)
s(135) =< aux(339)+aux(339)+aux(337)
s(120) =< it(27)*aux(59)
s(125) =< it(27)*aux(59)
s(124) =< it(26)*aux(59)
s(115) =< it(26)*aux(56)
s(135) =< it(26)*aux(59)
s(112) =< it(26)*aux(56)
s(122) =< it(26)*aux(65)
s(116) =< it(26)*aux(339)
s(123) =< s(124)
s(114) =< s(115)
s(134) =< s(135)
s(119) =< s(120)
s(113) =< s(116)

with precondition: [Out=0,V>=3,V1>=3]

* Chain [[26,27,28,29,30,38],32,40,45]: 18*it(26)+13*it(27)+2*s(112)+3*s(113)+8*s(114)+1*s(117)+4*s(119)+1*s(122)+28*s(123)+1*s(125)+3*s(134)+4*s(156)+10
Such that:aux(341) =< V
aux(342) =< V+V1
aux(343) =< V1
s(156) =< aux(341)
it(26) =< aux(342)
it(27) =< aux(342)
aux(59) =< aux(342)
aux(56) =< aux(343)
aux(65) =< aux(342)-1
it(26) =< aux(343)+aux(343)+aux(341)
s(117) =< it(27)*aux(342)
s(116) =< aux(343)+aux(343)+aux(341)
s(135) =< aux(343)+aux(343)+aux(341)
s(120) =< it(27)*aux(59)
s(125) =< it(27)*aux(59)
s(124) =< it(26)*aux(59)
s(115) =< it(26)*aux(56)
s(135) =< it(26)*aux(59)
s(112) =< it(26)*aux(56)
s(122) =< it(26)*aux(65)
s(116) =< it(26)*aux(343)
s(123) =< s(124)
s(114) =< s(115)
s(134) =< s(135)
s(119) =< s(120)
s(113) =< s(116)

with precondition: [Out=1,V>=3,V1>=3]

* Chain [[26,27,28,29,30,38],32,40,43]: 18*it(26)+13*it(27)+2*s(112)+3*s(113)+8*s(114)+1*s(117)+4*s(119)+1*s(122)+28*s(123)+1*s(125)+3*s(134)+4*s(156)+9
Such that:aux(345) =< V
aux(346) =< V+V1
aux(347) =< V1
s(156) =< aux(345)
it(26) =< aux(346)
it(27) =< aux(346)
aux(59) =< aux(346)
aux(56) =< aux(347)
aux(65) =< aux(346)-1
it(26) =< aux(347)+aux(347)+aux(345)
s(117) =< it(27)*aux(346)
s(116) =< aux(347)+aux(347)+aux(345)
s(135) =< aux(347)+aux(347)+aux(345)
s(120) =< it(27)*aux(59)
s(125) =< it(27)*aux(59)
s(124) =< it(26)*aux(59)
s(115) =< it(26)*aux(56)
s(135) =< it(26)*aux(59)
s(112) =< it(26)*aux(56)
s(122) =< it(26)*aux(65)
s(116) =< it(26)*aux(347)
s(123) =< s(124)
s(114) =< s(115)
s(134) =< s(135)
s(119) =< s(120)
s(113) =< s(116)

with precondition: [Out=0,V>=3,V1>=3]

* Chain [[26,27,28,29,30,38],31,[39,41],45]: 18*it(26)+10*it(27)+5*it(39)+9*it(41)+2*s(112)+3*s(113)+8*s(114)+1*s(117)+3*s(118)+4*s(119)+1*s(122)+28*s(123)+1*s(125)+3*s(134)+6
Such that:aux(13) =< 1
aux(350) =< V
aux(351) =< V+V1
aux(352) =< V+V1+1
aux(353) =< V1
it(41) =< aux(352)
it(39) =< aux(352)
it(39) =< aux(13)+aux(351)
it(26) =< aux(351)
it(27) =< aux(351)
s(121) =< aux(351)
it(26) =< aux(352)
it(27) =< aux(352)
s(121) =< aux(352)
aux(59) =< aux(351)
aux(56) =< aux(353)
aux(65) =< aux(351)-1
it(26) =< aux(353)+aux(353)+aux(350)
s(117) =< it(27)*aux(351)
s(116) =< aux(353)+aux(353)+aux(350)
s(135) =< aux(353)+aux(353)+aux(350)
s(120) =< it(27)*aux(59)
s(125) =< it(27)*aux(59)
s(124) =< it(26)*aux(59)
s(115) =< it(26)*aux(56)
s(135) =< it(26)*aux(59)
s(112) =< it(26)*aux(56)
s(122) =< it(26)*aux(65)
s(116) =< it(26)*aux(353)
s(123) =< s(124)
s(114) =< s(115)
s(134) =< s(135)
s(119) =< s(120)
s(118) =< s(121)
s(113) =< s(116)

with precondition: [Out=1,V>=2,V1>=2,V+V1>=6]

* Chain [[26,27,28,29,30,38],31,[39,41],43]: 18*it(26)+10*it(27)+5*it(39)+9*it(41)+2*s(112)+3*s(113)+8*s(114)+1*s(117)+3*s(118)+4*s(119)+1*s(122)+28*s(123)+1*s(125)+3*s(134)+5
Such that:aux(16) =< 1
aux(355) =< V
aux(356) =< V+V1
aux(357) =< V+V1+1
aux(358) =< V1
it(41) =< aux(357)
it(39) =< aux(357)
it(39) =< aux(16)+aux(356)
it(26) =< aux(356)
it(27) =< aux(356)
s(121) =< aux(356)
it(26) =< aux(357)
it(27) =< aux(357)
s(121) =< aux(357)
aux(59) =< aux(356)
aux(56) =< aux(358)
aux(65) =< aux(356)-1
it(26) =< aux(358)+aux(358)+aux(355)
s(117) =< it(27)*aux(356)
s(116) =< aux(358)+aux(358)+aux(355)
s(135) =< aux(358)+aux(358)+aux(355)
s(120) =< it(27)*aux(59)
s(125) =< it(27)*aux(59)
s(124) =< it(26)*aux(59)
s(115) =< it(26)*aux(56)
s(135) =< it(26)*aux(59)
s(112) =< it(26)*aux(56)
s(122) =< it(26)*aux(65)
s(116) =< it(26)*aux(358)
s(123) =< s(124)
s(114) =< s(115)
s(134) =< s(135)
s(119) =< s(120)
s(118) =< s(121)
s(113) =< s(116)

with precondition: [Out=0,V>=2,V1>=2,V+V1>=6]

* Chain [[26,27,28,29,30,38],31,[39,41],42,45]: 18*it(26)+10*it(27)+5*it(39)+18*it(41)+9*s(7)+2*s(112)+3*s(113)+8*s(114)+1*s(117)+3*s(118)+4*s(119)+1*s(122)+28*s(123)+1*s(125)+3*s(134)+10
Such that:aux(359) =< 1
aux(361) =< V
aux(362) =< V+V1
aux(363) =< V+V1+1
aux(364) =< V1
it(41) =< aux(363)
s(7) =< aux(359)
it(39) =< aux(363)
it(39) =< aux(359)+aux(362)
it(26) =< aux(362)
it(27) =< aux(362)
s(121) =< aux(362)
it(26) =< aux(363)
it(27) =< aux(363)
s(121) =< aux(363)
aux(59) =< aux(362)
aux(56) =< aux(364)
aux(65) =< aux(362)-1
it(26) =< aux(364)+aux(364)+aux(361)
s(117) =< it(27)*aux(362)
s(116) =< aux(364)+aux(364)+aux(361)
s(135) =< aux(364)+aux(364)+aux(361)
s(120) =< it(27)*aux(59)
s(125) =< it(27)*aux(59)
s(124) =< it(26)*aux(59)
s(115) =< it(26)*aux(56)
s(135) =< it(26)*aux(59)
s(112) =< it(26)*aux(56)
s(122) =< it(26)*aux(65)
s(116) =< it(26)*aux(364)
s(123) =< s(124)
s(114) =< s(115)
s(134) =< s(135)
s(119) =< s(120)
s(118) =< s(121)
s(113) =< s(116)

with precondition: [Out=1,V>=2,V1>=2,V+V1>=7]

* Chain [[26,27,28,29,30,38],31,[39,41],42,43]: 18*it(26)+10*it(27)+5*it(39)+18*it(41)+9*s(7)+2*s(112)+3*s(113)+8*s(114)+1*s(117)+3*s(118)+4*s(119)+1*s(122)+28*s(123)+1*s(125)+3*s(134)+9
Such that:aux(365) =< 1
aux(367) =< V
aux(368) =< V+V1
aux(369) =< V+V1+1
aux(370) =< V1
it(41) =< aux(369)
s(7) =< aux(365)
it(39) =< aux(369)
it(39) =< aux(365)+aux(368)
it(26) =< aux(368)
it(27) =< aux(368)
s(121) =< aux(368)
it(26) =< aux(369)
it(27) =< aux(369)
s(121) =< aux(369)
aux(59) =< aux(368)
aux(56) =< aux(370)
aux(65) =< aux(368)-1
it(26) =< aux(370)+aux(370)+aux(367)
s(117) =< it(27)*aux(368)
s(116) =< aux(370)+aux(370)+aux(367)
s(135) =< aux(370)+aux(370)+aux(367)
s(120) =< it(27)*aux(59)
s(125) =< it(27)*aux(59)
s(124) =< it(26)*aux(59)
s(115) =< it(26)*aux(56)
s(135) =< it(26)*aux(59)
s(112) =< it(26)*aux(56)
s(122) =< it(26)*aux(65)
s(116) =< it(26)*aux(370)
s(123) =< s(124)
s(114) =< s(115)
s(134) =< s(135)
s(119) =< s(120)
s(118) =< s(121)
s(113) =< s(116)

with precondition: [Out=0,V>=2,V1>=2,V+V1>=7]

* Chain [[26,27,28,29,30,38],31,[39,41],40,45]: 18*it(26)+10*it(27)+5*it(39)+9*it(41)+2*s(112)+3*s(113)+8*s(114)+1*s(117)+3*s(118)+4*s(119)+1*s(122)+28*s(123)+1*s(125)+3*s(134)+10
Such that:aux(31) =< 1
aux(372) =< V
aux(373) =< V+V1
aux(374) =< V+V1+1
aux(375) =< V1
it(41) =< aux(374)
it(39) =< aux(374)
it(39) =< aux(31)+aux(373)
it(26) =< aux(373)
it(27) =< aux(373)
s(121) =< aux(373)
it(26) =< aux(374)
it(27) =< aux(374)
s(121) =< aux(374)
aux(59) =< aux(373)
aux(56) =< aux(375)
aux(65) =< aux(373)-1
it(26) =< aux(375)+aux(375)+aux(372)
s(117) =< it(27)*aux(373)
s(116) =< aux(375)+aux(375)+aux(372)
s(135) =< aux(375)+aux(375)+aux(372)
s(120) =< it(27)*aux(59)
s(125) =< it(27)*aux(59)
s(124) =< it(26)*aux(59)
s(115) =< it(26)*aux(56)
s(135) =< it(26)*aux(59)
s(112) =< it(26)*aux(56)
s(122) =< it(26)*aux(65)
s(116) =< it(26)*aux(375)
s(123) =< s(124)
s(114) =< s(115)
s(134) =< s(135)
s(119) =< s(120)
s(118) =< s(121)
s(113) =< s(116)

with precondition: [Out=1,V>=2,V1>=2,V+V1>=7]

* Chain [[26,27,28,29,30,38],31,[39,41],40,43]: 18*it(26)+10*it(27)+5*it(39)+9*it(41)+2*s(112)+3*s(113)+8*s(114)+1*s(117)+3*s(118)+4*s(119)+1*s(122)+28*s(123)+1*s(125)+3*s(134)+9
Such that:aux(34) =< 1
aux(377) =< V
aux(378) =< V+V1
aux(379) =< V+V1+1
aux(380) =< V1
it(41) =< aux(379)
it(39) =< aux(379)
it(39) =< aux(34)+aux(378)
it(26) =< aux(378)
it(27) =< aux(378)
s(121) =< aux(378)
it(26) =< aux(379)
it(27) =< aux(379)
s(121) =< aux(379)
aux(59) =< aux(378)
aux(56) =< aux(380)
aux(65) =< aux(378)-1
it(26) =< aux(380)+aux(380)+aux(377)
s(117) =< it(27)*aux(378)
s(116) =< aux(380)+aux(380)+aux(377)
s(135) =< aux(380)+aux(380)+aux(377)
s(120) =< it(27)*aux(59)
s(125) =< it(27)*aux(59)
s(124) =< it(26)*aux(59)
s(115) =< it(26)*aux(56)
s(135) =< it(26)*aux(59)
s(112) =< it(26)*aux(56)
s(122) =< it(26)*aux(65)
s(116) =< it(26)*aux(380)
s(123) =< s(124)
s(114) =< s(115)
s(134) =< s(135)
s(119) =< s(120)
s(118) =< s(121)
s(113) =< s(116)

with precondition: [Out=0,V>=2,V1>=2,V+V1>=7]

* Chain [[26,27,28,29,30,38],31,45]: 18*it(26)+13*it(27)+2*s(112)+3*s(113)+8*s(114)+1*s(117)+4*s(119)+1*s(122)+28*s(123)+1*s(125)+3*s(134)+4*s(160)+6
Such that:aux(382) =< V
aux(383) =< V+V1
aux(384) =< V1
s(160) =< aux(384)
it(26) =< aux(383)
it(27) =< aux(383)
aux(59) =< aux(383)
aux(56) =< aux(384)
aux(65) =< aux(383)-1
it(26) =< aux(384)+aux(384)+aux(382)
s(117) =< it(27)*aux(383)
s(116) =< aux(384)+aux(384)+aux(382)
s(135) =< aux(384)+aux(384)+aux(382)
s(120) =< it(27)*aux(59)
s(125) =< it(27)*aux(59)
s(124) =< it(26)*aux(59)
s(115) =< it(26)*aux(56)
s(135) =< it(26)*aux(59)
s(112) =< it(26)*aux(56)
s(122) =< it(26)*aux(65)
s(116) =< it(26)*aux(384)
s(123) =< s(124)
s(114) =< s(115)
s(134) =< s(135)
s(119) =< s(120)
s(113) =< s(116)

with precondition: [Out=1,V>=2,V1>=2,V+V1>=5]

* Chain [[26,27,28,29,30,38],31,43]: 18*it(26)+13*it(27)+2*s(112)+3*s(113)+8*s(114)+1*s(117)+4*s(119)+1*s(122)+28*s(123)+1*s(125)+3*s(134)+4*s(160)+5
Such that:aux(386) =< V
aux(387) =< V+V1
aux(388) =< V1
s(160) =< aux(388)
it(26) =< aux(387)
it(27) =< aux(387)
aux(59) =< aux(387)
aux(56) =< aux(388)
aux(65) =< aux(387)-1
it(26) =< aux(388)+aux(388)+aux(386)
s(117) =< it(27)*aux(387)
s(116) =< aux(388)+aux(388)+aux(386)
s(135) =< aux(388)+aux(388)+aux(386)
s(120) =< it(27)*aux(59)
s(125) =< it(27)*aux(59)
s(124) =< it(26)*aux(59)
s(115) =< it(26)*aux(56)
s(135) =< it(26)*aux(59)
s(112) =< it(26)*aux(56)
s(122) =< it(26)*aux(65)
s(116) =< it(26)*aux(388)
s(123) =< s(124)
s(114) =< s(115)
s(134) =< s(135)
s(119) =< s(120)
s(113) =< s(116)

with precondition: [Out=0,V>=2,V1>=2,V+V1>=5]

* Chain [[26,27,28,29,30,38],31,42,45]: 18*it(26)+26*it(27)+9*s(7)+2*s(112)+3*s(113)+8*s(114)+1*s(117)+4*s(119)+1*s(122)+28*s(123)+1*s(125)+3*s(134)+10
Such that:aux(22) =< 1
aux(390) =< V
aux(391) =< V+V1
aux(392) =< V1
it(27) =< aux(391)
s(7) =< aux(22)
it(26) =< aux(391)
aux(59) =< aux(391)
aux(56) =< aux(392)
aux(65) =< aux(391)-1
it(26) =< aux(392)+aux(392)+aux(390)
s(117) =< it(27)*aux(391)
s(116) =< aux(392)+aux(392)+aux(390)
s(135) =< aux(392)+aux(392)+aux(390)
s(120) =< it(27)*aux(59)
s(125) =< it(27)*aux(59)
s(124) =< it(26)*aux(59)
s(115) =< it(26)*aux(56)
s(135) =< it(26)*aux(59)
s(112) =< it(26)*aux(56)
s(122) =< it(26)*aux(65)
s(116) =< it(26)*aux(392)
s(123) =< s(124)
s(114) =< s(115)
s(134) =< s(135)
s(119) =< s(120)
s(113) =< s(116)

with precondition: [Out=1,V>=2,V1>=2,V+V1>=6]

* Chain [[26,27,28,29,30,38],31,42,43]: 18*it(26)+26*it(27)+9*s(7)+2*s(112)+3*s(113)+8*s(114)+1*s(117)+4*s(119)+1*s(122)+28*s(123)+1*s(125)+3*s(134)+9
Such that:aux(22) =< 1
aux(394) =< V
aux(395) =< V+V1
aux(396) =< V1
it(27) =< aux(395)
s(7) =< aux(22)
it(26) =< aux(395)
aux(59) =< aux(395)
aux(56) =< aux(396)
aux(65) =< aux(395)-1
it(26) =< aux(396)+aux(396)+aux(394)
s(117) =< it(27)*aux(395)
s(116) =< aux(396)+aux(396)+aux(394)
s(135) =< aux(396)+aux(396)+aux(394)
s(120) =< it(27)*aux(59)
s(125) =< it(27)*aux(59)
s(124) =< it(26)*aux(59)
s(115) =< it(26)*aux(56)
s(135) =< it(26)*aux(59)
s(112) =< it(26)*aux(56)
s(122) =< it(26)*aux(65)
s(116) =< it(26)*aux(396)
s(123) =< s(124)
s(114) =< s(115)
s(134) =< s(135)
s(119) =< s(120)
s(113) =< s(116)

with precondition: [Out=0,V>=2,V1>=2,V+V1>=6]

* Chain [[26,27,28,29,30,38],31,40,45]: 18*it(26)+13*it(27)+2*s(112)+3*s(113)+8*s(114)+1*s(117)+4*s(119)+1*s(122)+28*s(123)+1*s(125)+3*s(134)+4*s(160)+10
Such that:aux(398) =< V
aux(399) =< V+V1
aux(400) =< V1
s(160) =< aux(400)
it(26) =< aux(399)
it(27) =< aux(399)
aux(59) =< aux(399)
aux(56) =< aux(400)
aux(65) =< aux(399)-1
it(26) =< aux(400)+aux(400)+aux(398)
s(117) =< it(27)*aux(399)
s(116) =< aux(400)+aux(400)+aux(398)
s(135) =< aux(400)+aux(400)+aux(398)
s(120) =< it(27)*aux(59)
s(125) =< it(27)*aux(59)
s(124) =< it(26)*aux(59)
s(115) =< it(26)*aux(56)
s(135) =< it(26)*aux(59)
s(112) =< it(26)*aux(56)
s(122) =< it(26)*aux(65)
s(116) =< it(26)*aux(400)
s(123) =< s(124)
s(114) =< s(115)
s(134) =< s(135)
s(119) =< s(120)
s(113) =< s(116)

with precondition: [Out=1,V>=2,V1>=2,V+V1>=6]

* Chain [[26,27,28,29,30,38],31,40,43]: 18*it(26)+13*it(27)+2*s(112)+3*s(113)+8*s(114)+1*s(117)+4*s(119)+1*s(122)+28*s(123)+1*s(125)+3*s(134)+4*s(160)+9
Such that:aux(402) =< V
aux(403) =< V+V1
aux(404) =< V1
s(160) =< aux(404)
it(26) =< aux(403)
it(27) =< aux(403)
aux(59) =< aux(403)
aux(56) =< aux(404)
aux(65) =< aux(403)-1
it(26) =< aux(404)+aux(404)+aux(402)
s(117) =< it(27)*aux(403)
s(116) =< aux(404)+aux(404)+aux(402)
s(135) =< aux(404)+aux(404)+aux(402)
s(120) =< it(27)*aux(59)
s(125) =< it(27)*aux(59)
s(124) =< it(26)*aux(59)
s(115) =< it(26)*aux(56)
s(135) =< it(26)*aux(59)
s(112) =< it(26)*aux(56)
s(122) =< it(26)*aux(65)
s(116) =< it(26)*aux(404)
s(123) =< s(124)
s(114) =< s(115)
s(134) =< s(135)
s(119) =< s(120)
s(113) =< s(116)

with precondition: [Out=0,V>=2,V1>=2,V+V1>=6]

* Chain [45]: 1
with precondition: [V=0,V1=Out,V1>=1]

* Chain [44]: 1
with precondition: [V1=0,V=Out,V>=1]

* Chain [43]: 0
with precondition: [Out=0,V>=0,V1>=0]

* Chain [42,45]: 9*s(7)+9*s(15)+5
Such that:aux(21) =< V
aux(22) =< V1
s(15) =< aux(21)
s(7) =< aux(22)

with precondition: [Out=1,V>=1,V1>=1]

* Chain [42,43]: 9*s(7)+9*s(15)+4
Such that:aux(21) =< V
aux(22) =< V1
s(15) =< aux(21)
s(7) =< aux(22)

with precondition: [Out=0,V>=1,V1>=1]

* Chain [40,45]: 5
with precondition: [V1=1,Out=1,V>=1]

* Chain [40,43]: 4
with precondition: [V1=1,Out=0,V>=1]

* Chain [37,45]: 5*s(139)+4*s(142)+5
Such that:aux(119) =< V1
aux(120) =< Out
s(139) =< aux(119)
s(142) =< aux(120)

with precondition: [Out>=2,V>=V1,V1>=Out]

* Chain [37,43]: 9*s(139)+4
Such that:aux(123) =< V1
s(139) =< aux(123)

with precondition: [Out=0,V1>=2,V>=V1]

* Chain [36,[39,41],45]: 5*it(39)+5*it(41)+1*s(149)+6
Such that:aux(13) =< 1
s(149) =< V1
aux(127) =< V
it(39) =< aux(127)
it(41) =< aux(127)
it(39) =< aux(13)+aux(127)

with precondition: [Out=1,V1>=2,V>=V1]

* Chain [36,[39,41],43]: 5*it(39)+5*it(41)+1*s(149)+5
Such that:aux(16) =< 1
s(149) =< V1
aux(131) =< V
it(39) =< aux(131)
it(41) =< aux(131)
it(39) =< aux(16)+aux(131)

with precondition: [Out=0,V1>=2,V>=V1]

* Chain [36,[39,41],42,45]: 5*it(39)+14*it(41)+9*s(7)+1*s(149)+10
Such that:s(149) =< V1
aux(135) =< 1
aux(136) =< V
it(41) =< aux(136)
s(7) =< aux(135)
it(39) =< aux(136)
it(39) =< aux(135)+aux(136)

with precondition: [Out=1,V>=3,V1>=2,V>=V1]

* Chain [36,[39,41],42,43]: 5*it(39)+14*it(41)+9*s(7)+1*s(149)+9
Such that:s(149) =< V1
aux(140) =< 1
aux(141) =< V
it(41) =< aux(141)
s(7) =< aux(140)
it(39) =< aux(141)
it(39) =< aux(140)+aux(141)

with precondition: [Out=0,V>=3,V1>=2,V>=V1]

* Chain [36,[39,41],40,45]: 5*it(39)+5*it(41)+1*s(149)+10
Such that:aux(31) =< 1
s(149) =< V1
aux(145) =< V
it(39) =< aux(145)
it(41) =< aux(145)
it(39) =< aux(31)+aux(145)

with precondition: [Out=1,V>=3,V1>=2,V>=V1]

* Chain [36,[39,41],40,43]: 5*it(39)+5*it(41)+1*s(149)+9
Such that:aux(34) =< 1
s(149) =< V1
aux(149) =< V
it(39) =< aux(149)
it(41) =< aux(149)
it(39) =< aux(34)+aux(149)

with precondition: [Out=0,V>=3,V1>=2,V>=V1]

* Chain [36,43]: 1*s(149)+5
Such that:s(149) =< V1

with precondition: [Out=0,V1>=2,V>=V1]

* Chain [36,42,45]: 9*s(7)+9*s(15)+1*s(149)+10
Such that:aux(22) =< 1
aux(21) =< V
s(149) =< V1
s(15) =< aux(21)
s(7) =< aux(22)

with precondition: [Out=1,V1>=2,V>=V1]

* Chain [36,42,43]: 9*s(7)+9*s(15)+1*s(149)+9
Such that:aux(22) =< 1
aux(21) =< V
s(149) =< V1
s(15) =< aux(21)
s(7) =< aux(22)

with precondition: [Out=0,V1>=2,V>=V1]

* Chain [36,40,45]: 1*s(149)+10
Such that:s(149) =< V1

with precondition: [Out=1,V1>=2,V>=V1]

* Chain [36,40,43]: 1*s(149)+9
Such that:s(149) =< V1

with precondition: [Out=0,V1>=2,V>=V1]

* Chain [35,[39,41],45]: 5*it(39)+5*it(41)+1*s(150)+6
Such that:aux(13) =< 1
s(150) =< V
aux(168) =< V1
it(39) =< aux(168)
it(41) =< aux(168)
it(39) =< aux(13)+aux(168)

with precondition: [Out=1,V>=2,V1>=V]

* Chain [35,[39,41],43]: 5*it(39)+5*it(41)+1*s(150)+5
Such that:aux(16) =< 1
s(150) =< V
aux(172) =< V1
it(39) =< aux(172)
it(41) =< aux(172)
it(39) =< aux(16)+aux(172)

with precondition: [Out=0,V>=2,V1>=V]

* Chain [35,[39,41],42,45]: 5*it(39)+14*it(41)+9*s(7)+1*s(150)+10
Such that:s(150) =< V
aux(176) =< 1
aux(177) =< V1
it(41) =< aux(177)
s(7) =< aux(176)
it(39) =< aux(177)
it(39) =< aux(176)+aux(177)

with precondition: [Out=1,V>=2,V1>=3,V1>=V]

* Chain [35,[39,41],42,43]: 5*it(39)+14*it(41)+9*s(7)+1*s(150)+9
Such that:s(150) =< V
aux(181) =< 1
aux(182) =< V1
it(41) =< aux(182)
s(7) =< aux(181)
it(39) =< aux(182)
it(39) =< aux(181)+aux(182)

with precondition: [Out=0,V>=2,V1>=3,V1>=V]

* Chain [35,[39,41],40,45]: 5*it(39)+5*it(41)+1*s(150)+10
Such that:aux(31) =< 1
s(150) =< V
aux(186) =< V1
it(39) =< aux(186)
it(41) =< aux(186)
it(39) =< aux(31)+aux(186)

with precondition: [Out=1,V>=2,V1>=3,V1>=V]

* Chain [35,[39,41],40,43]: 5*it(39)+5*it(41)+1*s(150)+9
Such that:aux(34) =< 1
s(150) =< V
aux(190) =< V1
it(39) =< aux(190)
it(41) =< aux(190)
it(39) =< aux(34)+aux(190)

with precondition: [Out=0,V>=2,V1>=3,V1>=V]

* Chain [35,43]: 1*s(150)+5
Such that:s(150) =< V

with precondition: [Out=0,V>=2,V1>=V]

* Chain [35,42,45]: 9*s(7)+9*s(15)+1*s(150)+10
Such that:aux(22) =< 1
s(150) =< V
aux(21) =< V1
s(15) =< aux(21)
s(7) =< aux(22)

with precondition: [Out=1,V>=2,V1>=V]

* Chain [35,42,43]: 9*s(7)+9*s(15)+1*s(150)+9
Such that:aux(22) =< 1
s(150) =< V
aux(21) =< V1
s(15) =< aux(21)
s(7) =< aux(22)

with precondition: [Out=0,V>=2,V1>=V]

* Chain [35,40,45]: 1*s(150)+10
Such that:s(150) =< V

with precondition: [Out=1,V>=2,V1>=V]

* Chain [35,40,43]: 1*s(150)+9
Such that:s(150) =< V

with precondition: [Out=0,V>=2,V1>=V]

* Chain [34,[39,41],45]: 5*it(39)+5*it(41)+4*s(151)+5
Such that:aux(13) =< 1
aux(12) =< V1+1
aux(210) =< V1
s(151) =< aux(210)
it(39) =< aux(12)
it(41) =< aux(12)
it(39) =< aux(13)+aux(210)

with precondition: [Out=1,V>=3,V1>=3]

* Chain [34,[39,41],43]: 5*it(39)+5*it(41)+4*s(151)+4
Such that:aux(16) =< 1
aux(15) =< V1+1
aux(213) =< V1
s(151) =< aux(213)
it(39) =< aux(15)
it(41) =< aux(15)
it(39) =< aux(16)+aux(213)

with precondition: [Out=0,V>=3,V1>=3]

* Chain [34,[39,41],42,45]: 5*it(39)+14*it(41)+9*s(7)+4*s(151)+9
Such that:aux(24) =< V1+1
aux(216) =< 1
aux(217) =< V1
s(151) =< aux(217)
it(41) =< aux(24)
s(7) =< aux(216)
it(39) =< aux(24)
it(39) =< aux(216)+aux(217)

with precondition: [Out=1,V>=4,V1>=4]

* Chain [34,[39,41],42,43]: 5*it(39)+14*it(41)+9*s(7)+4*s(151)+8
Such that:aux(27) =< V1+1
aux(220) =< 1
aux(221) =< V1
s(151) =< aux(221)
it(41) =< aux(27)
s(7) =< aux(220)
it(39) =< aux(27)
it(39) =< aux(220)+aux(221)

with precondition: [Out=0,V>=4,V1>=4]

* Chain [34,[39,41],40,45]: 5*it(39)+5*it(41)+4*s(151)+9
Such that:aux(31) =< 1
aux(30) =< V1+1
aux(224) =< V1
s(151) =< aux(224)
it(39) =< aux(30)
it(41) =< aux(30)
it(39) =< aux(31)+aux(224)

with precondition: [Out=1,V>=4,V1>=4]

* Chain [34,[39,41],40,43]: 5*it(39)+5*it(41)+4*s(151)+8
Such that:aux(34) =< 1
aux(33) =< V1+1
aux(227) =< V1
s(151) =< aux(227)
it(39) =< aux(33)
it(41) =< aux(33)
it(39) =< aux(34)+aux(227)

with precondition: [Out=0,V>=4,V1>=4]

* Chain [34,45]: 4*s(151)+5
Such that:aux(230) =< V1
s(151) =< aux(230)

with precondition: [Out=1,V>=2,V1>=2]

* Chain [34,43]: 4*s(151)+4
Such that:aux(234) =< V1
s(151) =< aux(234)

with precondition: [Out=0,V>=2,V1>=2]

* Chain [34,42,45]: 9*s(7)+13*s(15)+9
Such that:aux(22) =< 1
aux(238) =< V1
s(15) =< aux(238)
s(7) =< aux(22)

with precondition: [Out=1,V>=3,V1>=3]

* Chain [34,42,43]: 9*s(7)+13*s(15)+8
Such that:aux(22) =< 1
aux(242) =< V1
s(15) =< aux(242)
s(7) =< aux(22)

with precondition: [Out=0,V>=3,V1>=3]

* Chain [34,40,45]: 4*s(151)+9
Such that:aux(246) =< V1
s(151) =< aux(246)

with precondition: [Out=1,V>=3,V1>=3]

* Chain [34,40,43]: 4*s(151)+8
Such that:aux(250) =< V1
s(151) =< aux(250)

with precondition: [Out=0,V>=3,V1>=3]

* Chain [33,[39,41],45]: 5*it(39)+6*it(41)+5
Such that:aux(13) =< 1
aux(254) =< V
it(41) =< aux(254)
it(39) =< aux(254)
it(39) =< aux(13)+aux(254)

with precondition: [Out=1,V>=2,V1>=2]

* Chain [33,[39,41],43]: 5*it(39)+6*it(41)+4
Such that:aux(16) =< 1
aux(258) =< V
it(41) =< aux(258)
it(39) =< aux(258)
it(39) =< aux(16)+aux(258)

with precondition: [Out=0,V>=2,V1>=2]

* Chain [33,[39,41],42,45]: 5*it(39)+15*it(41)+9*s(7)+9
Such that:aux(262) =< 1
aux(263) =< V
it(41) =< aux(263)
s(7) =< aux(262)
it(39) =< aux(263)
it(39) =< aux(262)+aux(263)

with precondition: [Out=1,V>=3,V1>=3]

* Chain [33,[39,41],42,43]: 5*it(39)+15*it(41)+9*s(7)+8
Such that:aux(267) =< 1
aux(268) =< V
it(41) =< aux(268)
s(7) =< aux(267)
it(39) =< aux(268)
it(39) =< aux(267)+aux(268)

with precondition: [Out=0,V>=3,V1>=3]

* Chain [33,[39,41],40,45]: 5*it(39)+6*it(41)+9
Such that:aux(31) =< 1
aux(272) =< V
it(41) =< aux(272)
it(39) =< aux(272)
it(39) =< aux(31)+aux(272)

with precondition: [Out=1,V>=3,V1>=3]

* Chain [33,[39,41],40,43]: 5*it(39)+6*it(41)+8
Such that:aux(34) =< 1
aux(276) =< V
it(41) =< aux(276)
it(39) =< aux(276)
it(39) =< aux(34)+aux(276)

with precondition: [Out=0,V>=3,V1>=3]

* Chain [33,43]: 1*s(155)+4
Such that:s(155) =< V1

with precondition: [Out=0,V>=2,V1>=2]

* Chain [33,42,45]: 9*s(7)+10*s(15)+9
Such that:aux(22) =< 1
aux(283) =< V
s(15) =< aux(283)
s(7) =< aux(22)

with precondition: [Out=1,V>=2,V1>=2]

* Chain [33,42,43]: 9*s(7)+10*s(15)+8
Such that:aux(22) =< 1
aux(287) =< V
s(15) =< aux(287)
s(7) =< aux(22)

with precondition: [Out=0,V>=2,V1>=2]

* Chain [33,40,45]: 1*s(155)+9
Such that:s(155) =< V1

with precondition: [Out=1,V>=2,V1>=2]

* Chain [33,40,43]: 1*s(155)+8
Such that:s(155) =< V1

with precondition: [Out=0,V>=2,V1>=2]

* Chain [32,[39,41],45]: 5*it(39)+8*it(41)+1*s(156)+6
Such that:aux(13) =< 1
s(156) =< V
aux(11) =< V1
aux(298) =< V1+1
it(39) =< aux(298)
it(41) =< aux(298)
it(39) =< aux(13)+aux(11)

with precondition: [Out=1,V>=2,V1>=3,V1>=V]

* Chain [32,[39,41],43]: 5*it(39)+8*it(41)+1*s(156)+5
Such that:aux(16) =< 1
s(156) =< V
aux(14) =< V1
aux(302) =< V1+1
it(39) =< aux(302)
it(41) =< aux(302)
it(39) =< aux(16)+aux(14)

with precondition: [Out=0,V>=2,V1>=3,V1>=V]

* Chain [32,[39,41],42,45]: 5*it(39)+17*it(41)+9*s(7)+1*s(156)+10
Such that:s(156) =< V
aux(23) =< V1
aux(306) =< 1
aux(307) =< V1+1
it(41) =< aux(307)
s(7) =< aux(306)
it(39) =< aux(307)
it(39) =< aux(306)+aux(23)

with precondition: [Out=1,V>=2,V1>=4,V1>=V]

* Chain [32,[39,41],42,43]: 5*it(39)+17*it(41)+9*s(7)+1*s(156)+9
Such that:s(156) =< V
aux(26) =< V1
aux(311) =< 1
aux(312) =< V1+1
it(41) =< aux(312)
s(7) =< aux(311)
it(39) =< aux(312)
it(39) =< aux(311)+aux(26)

with precondition: [Out=0,V>=2,V1>=4,V1>=V]

* Chain [32,[39,41],40,45]: 5*it(39)+8*it(41)+1*s(156)+10
Such that:aux(31) =< 1
s(156) =< V
aux(29) =< V1
aux(316) =< V1+1
it(39) =< aux(316)
it(41) =< aux(316)
it(39) =< aux(31)+aux(29)

with precondition: [Out=1,V>=2,V1>=4,V1>=V]

* Chain [32,[39,41],40,43]: 5*it(39)+8*it(41)+1*s(156)+9
Such that:aux(34) =< 1
s(156) =< V
aux(32) =< V1
aux(320) =< V1+1
it(39) =< aux(320)
it(41) =< aux(320)
it(39) =< aux(34)+aux(32)

with precondition: [Out=0,V>=2,V1>=4,V1>=V]

* Chain [32,45]: 4*s(156)+6
Such that:aux(324) =< V1
s(156) =< aux(324)

with precondition: [Out=1,V=V1,V>=2]

* Chain [32,43]: 4*s(156)+5
Such that:aux(328) =< V
s(156) =< aux(328)

with precondition: [Out=0,V>=2,V1>=V]

* Chain [32,42,45]: 9*s(7)+12*s(15)+1*s(156)+10
Such that:aux(22) =< 1
s(156) =< V
aux(332) =< V1
s(15) =< aux(332)
s(7) =< aux(22)

with precondition: [Out=1,V>=2,V1>=3,V1>=V]

* Chain [32,42,43]: 9*s(7)+12*s(15)+1*s(156)+9
Such that:aux(22) =< 1
s(156) =< V
aux(336) =< V1
s(15) =< aux(336)
s(7) =< aux(22)

with precondition: [Out=0,V>=2,V1>=3,V1>=V]

* Chain [32,40,45]: 4*s(156)+10
Such that:aux(340) =< V
s(156) =< aux(340)

with precondition: [Out=1,V>=2,V1>=3,V1>=V]

* Chain [32,40,43]: 4*s(156)+9
Such that:aux(344) =< V
s(156) =< aux(344)

with precondition: [Out=0,V>=2,V1>=3,V1>=V]

* Chain [31,[39,41],45]: 5*it(39)+8*it(41)+1*s(160)+6
Such that:aux(13) =< 1
aux(11) =< V
s(160) =< V1
aux(349) =< V+1
it(39) =< aux(349)
it(41) =< aux(349)
it(39) =< aux(13)+aux(11)

with precondition: [Out=1,V>=3,V1>=2,V>=V1]

* Chain [31,[39,41],43]: 5*it(39)+8*it(41)+1*s(160)+5
Such that:aux(16) =< 1
aux(14) =< V
s(160) =< V1
aux(354) =< V+1
it(39) =< aux(354)
it(41) =< aux(354)
it(39) =< aux(16)+aux(14)

with precondition: [Out=0,V>=3,V1>=2,V>=V1]

* Chain [31,[39,41],42,45]: 5*it(39)+17*it(41)+9*s(7)+1*s(160)+10
Such that:aux(23) =< V
s(160) =< V1
aux(359) =< 1
aux(360) =< V+1
it(41) =< aux(360)
s(7) =< aux(359)
it(39) =< aux(360)
it(39) =< aux(359)+aux(23)

with precondition: [Out=1,V>=4,V1>=2,V>=V1]

* Chain [31,[39,41],42,43]: 5*it(39)+17*it(41)+9*s(7)+1*s(160)+9
Such that:aux(26) =< V
s(160) =< V1
aux(365) =< 1
aux(366) =< V+1
it(41) =< aux(366)
s(7) =< aux(365)
it(39) =< aux(366)
it(39) =< aux(365)+aux(26)

with precondition: [Out=0,V>=4,V1>=2,V>=V1]

* Chain [31,[39,41],40,45]: 5*it(39)+8*it(41)+1*s(160)+10
Such that:aux(31) =< 1
aux(29) =< V
s(160) =< V1
aux(371) =< V+1
it(39) =< aux(371)
it(41) =< aux(371)
it(39) =< aux(31)+aux(29)

with precondition: [Out=1,V>=4,V1>=2,V>=V1]

* Chain [31,[39,41],40,43]: 5*it(39)+8*it(41)+1*s(160)+9
Such that:aux(34) =< 1
aux(32) =< V
s(160) =< V1
aux(376) =< V+1
it(39) =< aux(376)
it(41) =< aux(376)
it(39) =< aux(34)+aux(32)

with precondition: [Out=0,V>=4,V1>=2,V>=V1]

* Chain [31,45]: 4*s(160)+6
Such that:aux(381) =< V1
s(160) =< aux(381)

with precondition: [Out=1,V=V1,V>=2]

* Chain [31,43]: 4*s(160)+5
Such that:aux(385) =< V1
s(160) =< aux(385)

with precondition: [Out=0,V1>=2,V>=V1]

* Chain [31,42,45]: 9*s(7)+12*s(15)+1*s(160)+10
Such that:aux(22) =< 1
s(160) =< V1
aux(389) =< V
s(15) =< aux(389)
s(7) =< aux(22)

with precondition: [Out=1,V>=3,V1>=2,V>=V1]

* Chain [31,42,43]: 9*s(7)+12*s(15)+1*s(160)+9
Such that:aux(22) =< 1
s(160) =< V1
aux(393) =< V
s(15) =< aux(393)
s(7) =< aux(22)

with precondition: [Out=0,V>=3,V1>=2,V>=V1]

* Chain [31,40,45]: 4*s(160)+10
Such that:aux(397) =< V1
s(160) =< aux(397)

with precondition: [Out=1,V>=3,V1>=2,V>=V1]

* Chain [31,40,43]: 4*s(160)+9
Such that:aux(401) =< V1
s(160) =< aux(401)

with precondition: [Out=0,V>=3,V1>=2,V>=V1]


#### Cost of chains of start(V,V1):
* Chain [48]: 310*s(2511)+229*s(2513)+468*s(2526)+30*s(2527)+66*s(2528)+60*s(2529)+114*s(2530)+60*s(2531)+30*s(2532)+1383*s(2533)+1134*s(2534)+69*s(2538)+69*s(2542)+126*s(2545)+63*s(2546)+1764*s(2547)+504*s(2548)+189*s(2549)+276*s(2550)+189*s(2551)+144*s(2552)+60*s(2553)+108*s(2554)+120*s(2555)+12*s(2557)+12*s(2561)+12*s(2564)+6*s(2565)+168*s(2566)+48*s(2567)+18*s(2568)+48*s(2569)+36*s(2570)+18*s(2571)+108*s(2572)+12*s(2578)+6*s(2579)+168*s(2580)+48*s(2581)+18*s(2582)+18*s(2583)+120*s(2584)+108*s(2585)+12*s(2590)+6*s(2591)+168*s(2592)+48*s(2593)+18*s(2594)+18*s(2595)+30*s(2596)+30*s(2597)+10
Such that:aux(427) =< 1
aux(428) =< V
aux(429) =< V+1
aux(430) =< V+V1
aux(431) =< V+V1+1
aux(432) =< V1
aux(433) =< V1+1
s(2513) =< aux(428)
s(2511) =< aux(432)
s(2526) =< aux(427)
s(2527) =< aux(429)
s(2528) =< aux(429)
s(2527) =< aux(427)+aux(428)
s(2529) =< aux(433)
s(2530) =< aux(433)
s(2529) =< aux(427)+aux(432)
s(2531) =< aux(428)
s(2531) =< aux(427)+aux(428)
s(2532) =< aux(432)
s(2532) =< aux(427)+aux(432)
s(2533) =< aux(430)
s(2534) =< aux(430)
s(2535) =< aux(430)
s(2536) =< aux(432)
s(2537) =< aux(430)-1
s(2534) =< aux(432)+aux(432)+aux(428)
s(2538) =< s(2533)*aux(430)
s(2539) =< aux(432)+aux(432)+aux(428)
s(2540) =< aux(432)+aux(432)+aux(428)
s(2541) =< s(2533)*s(2535)
s(2542) =< s(2533)*s(2535)
s(2543) =< s(2534)*s(2535)
s(2544) =< s(2534)*s(2536)
s(2540) =< s(2534)*s(2535)
s(2545) =< s(2534)*s(2536)
s(2546) =< s(2534)*s(2537)
s(2539) =< s(2534)*aux(432)
s(2547) =< s(2543)
s(2548) =< s(2544)
s(2549) =< s(2540)
s(2550) =< s(2541)
s(2551) =< s(2539)
s(2552) =< aux(431)
s(2553) =< aux(431)
s(2553) =< aux(427)+aux(430)
s(2554) =< aux(430)
s(2555) =< aux(430)
s(2556) =< aux(430)
s(2554) =< aux(431)
s(2555) =< aux(431)
s(2556) =< aux(431)
s(2554) =< aux(432)+aux(432)+aux(428)
s(2557) =< s(2555)*aux(430)
s(2558) =< aux(432)+aux(432)+aux(428)
s(2559) =< aux(432)+aux(432)+aux(428)
s(2560) =< s(2555)*s(2535)
s(2561) =< s(2555)*s(2535)
s(2562) =< s(2554)*s(2535)
s(2563) =< s(2554)*s(2536)
s(2559) =< s(2554)*s(2535)
s(2564) =< s(2554)*s(2536)
s(2565) =< s(2554)*s(2537)
s(2558) =< s(2554)*aux(432)
s(2566) =< s(2562)
s(2567) =< s(2563)
s(2568) =< s(2559)
s(2569) =< s(2560)
s(2570) =< s(2556)
s(2571) =< s(2558)
s(2572) =< aux(430)
s(2572) =< aux(431)
s(2573) =< aux(432)
s(2573) =< aux(433)
s(2572) =< s(2573)+s(2573)+aux(428)
s(2574) =< s(2573)+s(2573)+aux(428)
s(2575) =< s(2573)+s(2573)+aux(428)
s(2576) =< s(2572)*s(2535)
s(2577) =< s(2572)*s(2536)
s(2575) =< s(2572)*s(2535)
s(2578) =< s(2572)*s(2536)
s(2579) =< s(2572)*s(2537)
s(2574) =< s(2572)*aux(432)
s(2580) =< s(2576)
s(2581) =< s(2577)
s(2582) =< s(2575)
s(2583) =< s(2574)
s(2584) =< aux(430)
s(2584) =< aux(427)+aux(430)
s(2585) =< aux(430)
s(2585) =< s(2573)+s(2573)+aux(428)
s(2586) =< s(2573)+s(2573)+aux(428)
s(2587) =< s(2573)+s(2573)+aux(428)
s(2588) =< s(2585)*s(2535)
s(2589) =< s(2585)*s(2536)
s(2587) =< s(2585)*s(2535)
s(2590) =< s(2585)*s(2536)
s(2591) =< s(2585)*s(2537)
s(2586) =< s(2585)*aux(432)
s(2592) =< s(2588)
s(2593) =< s(2589)
s(2594) =< s(2587)
s(2595) =< s(2586)
s(2596) =< aux(430)
s(2596) =< aux(430)+aux(430)
s(2597) =< aux(430)
s(2597) =< aux(432)+aux(428)

with precondition: [V>=0,V1>=0]

* Chain [47]: 1
with precondition: [V1=0,V>=0]

* Chain [46]: 8*s(2727)+6
Such that:s(2726) =< V1
s(2727) =< s(2726)

with precondition: [V=V1,V>=2]


Closed-form bounds of start(V,V1):
-------------------------------------
* Chain [48] with precondition: [V>=0,V1>=0]
- Upper bound: 775*V+1312*V1+478+ (V+V1)* (810*V1)+ (V+V1)* (nat(V+V1-1)*81)+ (3177*V+3177*V1)+ (2754*V+2754*V1)* (V+V1)+ (96*V+96)+ (174*V1+174)+ (204*V+204*V1+204)
- Complexity: n^2
* Chain [47] with precondition: [V1=0,V>=0]
- Upper bound: 1
- Complexity: constant
* Chain [46] with precondition: [V=V1,V>=2]
- Upper bound: 8*V1+6
- Complexity: n

### Maximum cost of start(V,V1): 775*V+1304*V1+472+ (V+V1)* (810*V1)+ (V+V1)* (nat(V+V1-1)*81)+ (3177*V+3177*V1)+ (2754*V+2754*V1)* (V+V1)+ (96*V+96)+ (174*V1+174)+ (204*V+204*V1+204)+ (8*V1+5)+1
Asymptotic class: n^2
* Total analysis performed in 10195 ms.

(12) BOUNDS(1, n^2)